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

Goal state before:
pp: A : Type u_1
𝕜 : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : PartialOrder A
inst✝³ : Semifield 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Algebra 𝕜 A
inst✝ : PosSMulMono 𝕜 A
c : 𝕜
hc : 0 < c
a : A
ha : IsStrictlyPositive a
⊢ IsStrictlyPositive (c • a)

Tactic:
have hunit : IsUnit (c • a) :=
    isUnit_iff_exists.mpr ⟨c⁻¹ • ha.isUnit.unit⁻¹, by simp [(ne_of_lt hc).symm]⟩

Goal state after:
A : Type u_1
𝕜 : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : PartialOrder A
inst✝³ : Semifield 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Algebra 𝕜 A
inst✝ : PosSMulMono 𝕜 A
c : 𝕜
hc : 0 < c
a : A
ha : IsStrictlyPositive a
hunit : IsUnit (c • a)
⊢ IsStrictlyPositive (c • a)
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: case mp
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
w : A ⊗[R] B
⊢ w ∈ centralizer R (⇑includeLeft '' S) → w ∈ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).range

pp: case mpr
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
w : A ⊗[R] B
⊢ w ∈ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).range → w ∈ centralizer R (⇑includeLeft '' S)

Tactic:
· intro hw
    rw [mem_centralizer_iff] at hw
    let ℬ := Module.Free.chooseBasis R B
    obtain ⟨b, rfl⟩ := TensorProduct.eq_repr_basis_right ℬ w
    refine Subalgebra.sum_mem _ fun j hj => ⟨⟨b j, ?_⟩ ⊗ₜ[R] ℬ j, by simp⟩
    rw [Subalgebra.mem_centralizer_iff]
    intro x hx
    suffices x • b = b.mapRange (· * x) (by simp) from Finsupp.ext_iff.1 this j
    specialize hw (x ⊗ₜ[R] 1) ⟨x, hx, rfl⟩
    simp only [Finsupp.sum, Finset.mul_sum, Algebra.TensorProduct.tmul_mul_tmul, one_mul,
      Finset.sum_mul, mul_one] at hw
    refine TensorProduct.sum_tmul_basis_right_injective ℬ ?_
    simp only [Finsupp.coe_lsum]
    rw [sum_of_support_subset (s := b.support) (hs := Finsupp.support_smul) (h := by simp),
      sum_of_support_subset (s := b.support) (hs := support_mapRange) (h := by simp)]
    simpa only [Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, LinearMap.flip_apply,
      TensorProduct.mk_apply, Finsupp.mapRange_apply] using hw

Goal state after:
case mpr
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
w : A ⊗[R] B
⊢ w ∈ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).range → w ∈ centralizer R (⇑includeLeft '' S)
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
⊢ Module.rank R (M ⧸ M') + Module.rank R ↥M' ≤ Module.rank R M

Tactic:
conv_lhs => simp only [Module.rank_def]
  rw [Cardinal.ciSup_add_ciSup _ bddAbove_of_small _ bddAbove_of_small]
  refine ciSup_le fun ⟨s, hs⟩ ↦ ciSup_le fun ⟨t, ht⟩ ↦ ?_
  choose f hf using Submodule.Quotient.mk_surjective M'
  simpa [add_comm] using! (LinearIndependent.sumElim_of_quotient ht (fun (i : s) ↦ f i)
    (by simpa [Function.comp_def, hf] using! hs)).cardinal_le_rank

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

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
⊢ Module.rank R M = 0

Tactic:
rw [← nonpos_iff_eq_zero, Module.rank_def]

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
⊢ ⨆ ι, #↑↑ι ≤ 0
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : Module R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : Module R C
inst✝³ : Star C
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F R A B
inst✝ : StarHomClass F A B
S✝ : NonUnitalStarSubalgebra R A
f : F
S : NonUnitalStarSubalgebra R A
a : A
ha : a ∈ ↑S.toNonUnitalSubsemiring
⊢ star (↑(NonUnitalAlgHomClass.toNonUnitalAlgHom f) a) ∈
    (NonUnitalSubalgebra.map (NonUnitalAlgHomClass.toNonUnitalAlgHom f) S.toNonUnitalSubalgebra).carrier

Tactic:
exact ⟨star a, star_mem (s := S) ha, map_star f a⟩

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f : E →ₛₗ.[σ] F
x : ↥⊥.domain
y : ↥f.domain
h : ↑x = ↑y
⊢ ↑⊥ x = ↑f y

Tactic:
have hx : x = 0 := Subtype.ext ((mem_bot R).1 x.2)
      have hy : y = 0 := Subtype.ext (h.symm.trans (congr_arg _ hx))
      rw [hx, hy, map_zero, map_zero]

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
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
f g : End K (Fin n → K)
hfg : f * g = 1
⊢ g * f = 1

Tactic:
have ginj : Injective g :=
    HasLeftInverse.injective ⟨f, fun x => show (f * g) x = (1 : End K (Fin n → K)) x by rw [hfg]⟩

Goal state after:
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
⊢ g * f = 1
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₂
R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : IsStablyFiniteRing R
e : M ≃ₗ[R] Free.ChooseBasisIndex R M → R :=
  (Free.chooseBasis R M).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite R R (Free.ChooseBasisIndex R M)
⊢ IsStablyFiniteRing (End R M)

Tactic:
RingEquiv.isStablyFiniteRing_iff e.conjRingEquiv

Goal state after:
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₂
R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : IsStablyFiniteRing R
e : M ≃ₗ[R] Free.ChooseBasisIndex R M → R :=
  (Free.chooseBasis R M).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite R R (Free.ChooseBasisIndex R M)
⊢ IsStablyFiniteRing (End R (Free.ChooseBasisIndex R M → R))
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case refine_1
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
⊢ finrank K ↥S = 1

Tactic:
suffices K ∙ v = S by rw [← this, finrank_span_singleton hv_ne]

Goal state after:
case refine_1
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
⊢ K ∙ v = S
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✝ : Free F E
⊢ finrank F E = 1 ↔ Function.Bijective ⇑(algebraMap F E)

Tactic:
refine ⟨?_, Module.finrank_of_bijective_algebraMap⟩
  nontriviality E
  refine fun h ↦ ⟨FaithfulSMul.algebraMap_injective F E, ?_⟩
  rwa [Algebra.surjective_algebraMap_iff, eq_comm, Subalgebra.bot_eq_top_iff_finrank_eq_one]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ Algebra.adjoin R s = ((lift R) Subtype.val).range

Tactic:
by
  rw [← Algebra.adjoin_range_eq_range_freeAlgebra_lift, Subtype.range_coe]

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

Goal state before:
pp: n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
mlt : 0 < n
mdvd : n = 0
⊢ False

Tactic:
exact mlt.ne' mdvd

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

Goal state before:
pp: case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : k ∣ n
⊢ n.minFacProp (if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))

Tactic:
simp only [k, dk, ↓reduceIte]

Goal state after:
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : k ∣ n
⊢ n.minFacProp x✝
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
⊢ n.minFacProp (if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))

Tactic:
simp only [k, dk, ↓reduceIte]

Goal state after:
case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
⊢ n.minFacProp (n.minFacAux (x✝ + 2))
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this✝ : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : (2 * i + 3).succ ∣ n
ml : x✝ < m
me : x✝.succ = m
d' : 2 * (i + 2) ∣ n
this : x✝ ≤ 2
⊢ False

Tactic:
rw [e] at this

Goal state after:
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this✝ : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : (2 * i + 3).succ ∣ n
ml : x✝ < m
me : x✝.succ = m
d' : 2 * (i + 2) ∣ n
this : 2 * i + 3 ≤ 2
⊢ False
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
pos : 0 < n
np : ¬2 ≤ n ∨ False
h1 : n = n.minFac
⊢ n.minFac ≤ n / n.minFac

Tactic:
_root_.or_false,

Goal state after:
n : ℕ
pos : 0 < n
np : ¬2 ≤ n
h1 : n = n.minFac
⊢ n.minFac ≤ n / n.minFac
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
ι : Type u_1
l : List ι
f : ι → R[X]
n : ℕ
⊢ (List.map (⇑(lcoeff R n)) (List.map f l)).sum = (List.map (fun a ↦ (f a).coeff n) l).sum

Tactic:
List.map_map,

Goal state after:
R : Type u
inst✝ : Semiring R
ι : Type u_1
l : List ι
f : ι → R[X]
n : ℕ
⊢ (List.map (⇑(lcoeff R n) ∘ f) l).sum = (List.map (fun a ↦ (f a).coeff n) l).sum
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.degree = ↑n
⊢ p.natDegree = n

Tactic:
rw [natDegree, h, Nat.cast_withBot, WithBot.unbotD_coe]

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

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ
⊢ r ∣ (C r * φ).coeff c

Tactic:
coeff_C_mul

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ
⊢ r ∣ r * φ.coeff c
Module: Mathlib.Algebra.Polynomial.Degree.Support

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < ↑n
hp : p = 0
⊢ ∑ i, f (↑i) (p.coeff ↑i) = p.sum f

pp: case neg
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < ↑n
hp : ¬p = 0
⊢ ∑ i, f (↑i) (p.coeff ↑i) = p.sum f

Tactic:
· rw [hp, sum_zero_index, Finset.sum_eq_zero]
    intro i _
    exact hf i

Goal state after:
case neg
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < ↑n
hp : ¬p = 0
⊢ ∑ i, f (↑i) (p.coeff ↑i) = p.sum f
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case h₁
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
h : ap ∉ p.coeff.support
a : A
x✝¹ : a ∈ q.coeff.support
x✝ : ap + a = ap + aq
⊢ p.coeff ap * q.coeff a = 0

Tactic:
rw [Finsupp.notMem_support_iff.mp h, zero_mul]

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✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
⊢ leadingCoeff D (single a r) = r

Tactic:
by
  rw [leadingCoeff, supDegree_single]
  split_ifs with hr
  · simp [hr]
  · rw [Function.leftInverse_invFun hD]
    simp

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Ring R
p : R[X]
hp : 0 < p.degree
⊢ (p - C a).degree = p.degree

Tactic:
by
  rw [sub_eq_add_neg, ← C_neg, degree_add_C hp]

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
p : R[X]
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T
g : S →+* T
x : T
⊢ eval₂ g x (map f p) = eval₂ (g.comp f) x p

Tactic:
eval₂_eq_eval_map,

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
p : R[X]
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T
g : S →+* T
x : T
⊢ eval x (map g (map f p)) = eval₂ (g.comp f) x p
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
p : R[X]
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T
g : S →+* T
x : T
⊢ eval x (map g (map f p)) = eval₂ (g.comp f) x p

Tactic:
eval₂_eq_eval_map,

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
p : R[X]
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T
g : S →+* T
x : T
⊢ eval x (map g (map f p)) = eval x (map (g.comp f) p)
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hq : Monic D q
⊢ leadingCoeff D (0 * q) = leadingCoeff D 0

pp: case inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hq : Monic D q
hp : p ≠ 0
⊢ leadingCoeff D (p * q) = leadingCoeff D p

Tactic:
· rw [zero_mul]

Goal state after:
case inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hq : Monic D q
hp : p ≠ 0
⊢ leadingCoeff D (p * q) = leadingCoeff D p
Module: Mathlib.Algebra.Polynomial.Monomial

Goal state before:
pp: case h₁
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
x✝ : R
⊢ (f'.comp AddMonoidAlgebra.singleZeroRingHom) x✝ = (g'.comp AddMonoidAlgebra.singleZeroRingHom) x✝

Tactic:
simp [f', g', h₁, RingEquiv.toRingHom_eq_coe]

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

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
a b : R
inst✝ : Invertible a
p : R[X]
⊢ C ⅟a * (X - C b) = C ⅟a * X + -(C ⅟a * C b)

Tactic:
simp [mul_add, sub_eq_add_neg]

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝¹ : LinearOrder ι
inst✝ : (a : ι) → PartialOrder (β a)
a b c : Lex ((i : ι) → β i)
N₁ : ι
lt_N₁ : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j N₁ → a j = b j
a_lt_b : a N₁ < b N₁
N₂ : ι
lt_N₂ : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j N₂ → b j = c j
b_lt_c : b N₂ < c N₂
⊢ a < c

Tactic:
rcases lt_trichotomy N₁ N₂ with (H | rfl | H)

Goal state after:
case inl
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝¹ : LinearOrder ι
inst✝ : (a : ι) → PartialOrder (β a)
a b c : Lex ((i : ι) → β i)
N₁ : ι
lt_N₁ : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j N₁ → a j = b j
a_lt_b : a N₁ < b N₁
N₂ : ι
lt_N₂ : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j N₂ → b j = c j
b_lt_c : b N₂ < c N₂
H : N₁ < N₂
⊢ a < c

case inr.inl
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝¹ : LinearOrder ι
inst✝ : (a : ι) → PartialOrder (β a)
a b c : Lex ((i : ι) → β i)
N₁ : ι
lt_N₁ : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j N₁ → a j = b j
a_lt_b : a N₁ < b N₁
lt_N₂ : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j N₁ → b j = c j
b_lt_c : b N₁ < c N₁
⊢ a < c

case inr.inr
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝¹ : LinearOrder ι
inst✝ : (a : ι) → PartialOrder (β a)
a b c : Lex ((i : ι) → β i)
N₁ : ι
lt_N₁ : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j N₁ → a j = b j
a_lt_b : a N₁ < b N₁
N₂ : ι
lt_N₂ : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j N₂ → b j = c j
b_lt_c : b N₂ < c N₂
H : N₂ < N₁
⊢ a < c
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
a : R
⊢ p ∣ q.comp (X - C a) ↔ p.comp (X + C a) ∣ q

Tactic:
by
  let _ := invertibleOne (α := R)
  simpa using! dvd_comp_C_mul_X_add_C_iff p q 1 (-a)

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
P : R[X]
⊢ P ∈ R[X]⁰ ↔ ∀ (a : R), a • P = 0 → a = 0

Tactic:
simpa [not_imp_not] using (notMem_nonZeroDivisors_iff (P := P)).not

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 : σ →₀ ℕ
k : ℕ
⊢ coeff m (X i ^ k) = if Finsupp.single i k = m then 1 else 0

Tactic:
by
  have := coeff_monomial m (Finsupp.single i k) (1 : R)
  rwa [@monomial_eq _ _ (1 : R) (Finsupp.single i k) _, C_1, one_mul, Finsupp.prod_single_index]
    at this
  exact pow_zero _

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

Goal state before:
pp: case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
c : σ →₀ ℕ
⊢ r ∣ coeff c (C r * φ)

Tactic:
coeff_C_mul

Goal state after:
case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
c : σ →₀ ℕ
⊢ r ∣ r * coeff c φ
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ p.vars = p.degrees.toFinset

Tactic:
rw [vars]
  convert! rfl

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ p.vars = p.support.biUnion Finsupp.support

Tactic:
by
  ext i
  rw [mem_vars_iff_mem_support, Finset.mem_biUnion]

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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
s : Set S₁
⊢ Algebra.adjoin R s = (aeval Subtype.val).range

Tactic:
rw [← Algebra.adjoin_range_eq_range_aeval, Subtype.range_coe]

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

Goal state before:
pp: 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
⊢ eval₂ f v p ∈ s

Tactic:
replace hs : ∀ i, f (p.coeff i) ∈ s := by
    intro i
    by_cases hi : i ∈ p.support
    · exact hs i hi
    · rw [MvPolynomial.notMem_support_iff.1 hi, f.map_zero]
      exact zero_mem s

Goal state after:
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
v : σ → S
hv : ∀ (i : σ), v i ∈ s
hs : ∀ (i : σ →₀ ℕ), f (coeff i p) ∈ s
⊢ eval₂ f v p ∈ s
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ (q + p).totalDegree = p.totalDegree

Tactic:
by
  rw [add_comm, totalDegree_add_eq_left_of_totalDegree_lt h]

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ (C a * p).coeff p.natDegree ≠ 0

Tactic:
coeff_C_mul

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ a * p.coeff p.natDegree ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case neg
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)
hi : p.natTrailingDegree ≤ i
hj : q.natTrailingDegree ≤ j
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
refine (h₂ (Prod.ext_iff.mpr ?_).symm).elim

Goal state after:
case neg
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)
hi : p.natTrailingDegree ≤ i
hj : q.natTrailingDegree ≤ j
⊢ (p.natTrailingDegree, q.natTrailingDegree).1 = (i, j).1 ∧ (p.natTrailingDegree, q.natTrailingDegree).2 = (i, j).2
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ reflect n 1 = X ^ n

Tactic:
rw [← C.map_one, reflect_C, map_one, one_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
hlead : f.eraseLead ≠ 0
hnext : f.nextCoeff = 0
⊢ 2 ≤ f.natDegree

Tactic:
by
  contrapose! hlead
  rw [Nat.lt_succ_iff, Nat.le_one_iff_eq_zero_or_eq_one, natDegree_eq_zero, natDegree_eq_one]
    at hlead
  obtain ⟨a, rfl⟩ | ⟨a, ha, b, rfl⟩ := hlead
  · simp
  · rw [nextCoeff_C_mul_X_add_C ha] at hnext
    subst b
    simp

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

Goal state before:
pp: case neg
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
he₂ : ¬((X - C x) * P).eraseLead = 0
h₂ : #(X - C x).support = 2
hmul : #((X - C x) * P).support ≤ #(X - C x).support * #P.support
⊢ #((X - C x) * P).support ≤ 2

Tactic:
h₂

Goal state after:
case neg
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
he₂ : ¬((X - C x) * P).eraseLead = 0
h₂ : #(X - C x).support = 2
hmul : #((X - C x) * P).support ≤ 2 * #P.support
⊢ #((X - C x) * P).support ≤ 2