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

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst✝³ : Nonempty ι
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → NonUnitalRing (κ i)
inst✝ : (i : ι) → Module R (κ i)
a : (i : ι) → κ i
r : R
hr : IsUnit r
⊢ (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔ ∃ i, ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a i))

Tactic:
lift r to Rˣ using hr with r' hr'

Goal state after:
case pos
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst✝³ : Nonempty ι
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → NonUnitalRing (κ i)
inst✝ : (i : ι) → Module R (κ i)
a : (i : ι) → κ i
r : R
r' : Rˣ
hr' : ↑r' = r
⊢ (∀ (hr : IsUnit ↑r'), ¬IsQuasiregular (-(⋯.unit⁻¹ • a))) ↔
    ∃ i, ∀ (hr : IsUnit ↑r'), ¬IsQuasiregular (-(⋯.unit⁻¹ • a i))
Module: Mathlib.Algebra.Algebra.Spectrum.Pi

Goal state before:
pp: case pos
A : Type u_2
B : Type u_3
R : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : NonUnitalRing B
inst✝¹ : Module R A
inst✝ : Module R B
a : A
b : B
r : R
hr : IsUnit r
⊢ (∃ (h : IsUnit r), IsQuasiregular (-(⋯.unit⁻¹ • (a, b)))) ↔
    ¬((∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ∨ ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • b)))

Tactic:
lift r to Rˣ using hr with r' hr'

Goal state after:
case pos
A : Type u_2
B : Type u_3
R : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : NonUnitalRing B
inst✝¹ : Module R A
inst✝ : Module R B
a : A
b : B
r : R
r' : Rˣ
hr' : ↑r' = r
⊢ (∃ (h : IsUnit ↑r'), IsQuasiregular (-(⋯.unit⁻¹ • (a, b)))) ↔
    ¬((∀ (hr : IsUnit ↑r'), ¬IsQuasiregular (-(⋯.unit⁻¹ • a))) ∨ ∀ (hr : IsUnit ↑r'), ¬IsQuasiregular (-(⋯.unit⁻¹ • b)))
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
M' : Submodule R M
s : Set M
hs : s ⊆ ↑M'
hs' : LinearIndepOn R id s
t : Set M
ht : LinearIndepOn R (⇑M'.mkQ) t
⊢ LinearIndepOn R (⇑(span R (id '' s)).mkQ ∘ id) t

Tactic:
image_id

Goal state after:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
s : Set M
hs : s ⊆ ↑M'
hs' : LinearIndepOn R id s
t : Set M
ht : LinearIndepOn R (⇑M'.mkQ) t
⊢ LinearIndepOn R (⇑(span R s).mkQ ∘ id) t
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: case e'_3.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 B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
⊢ (∃ x_1,
      (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) x_1 = (Algebra.TensorProduct.comm R A B) x) →
    ∃ x_1, (Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R S).val) x_1 = x

Tactic:
· rintro ⟨y, hy⟩
      refine ⟨(Algebra.TensorProduct.comm R _ _) y, (Algebra.TensorProduct.comm R A B).injective ?_⟩
      rw [← hy, comm_comp_map_apply, ← Algebra.TensorProduct.comm_symm, AlgEquiv.symm_apply_apply]

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

Goal state before:
pp: R✝ : Type u_1
A : Type u_2
inst✝⁷ : NonUnitalRing R✝
inst✝⁶ : PartialOrder R✝
inst✝⁵ : StarRing R✝
inst✝⁴ : StarOrderedRing R✝
p q : R✝
R : Type u_3
inst✝³ : NonUnitalRing R
inst✝² : LinearOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
r : R
⊢ star r = r

Tactic:
obtain (hr | hr) : 0 ≤ r ∨ 0 ≤ -r := by grind
    · exact hr.star_eq
    · simpa using hr.star_eq

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

Goal state before:
pp: R : Type u
S : Type u'
M : Type v
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : StrongRankCondition S
inst✝⁵ : Module S M
inst✝⁴ : Module S M'
inst✝³ : Free S M'
inst✝² : Algebra S R
inst✝¹ : IsScalarTower S R M
inst✝ : Free R M
⊢ Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')

Tactic:
obtain ⟨⟨_, bM⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
  obtain ⟨⟨_, bN⟩⟩ := Module.Free.exists_basis (R := S) (M := M')
  rw [← bM.mk_eq_rank'', ← bN.mk_eq_rank'', ← (bM.tensorProduct bN).mk_eq_rank'', Cardinal.mk_prod]

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
⊢ (∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0) → Module.rank R M = 0

Tactic:
intro h
    rw [← nonpos_iff_eq_zero, Module.rank_def]
    apply ciSup_le'
    intro ⟨s, hs⟩
    rw [nonpos_iff_eq_zero, Cardinal.mk_eq_zero_iff, ← not_nonempty_iff]
    rintro ⟨i : s⟩
    obtain ⟨a, ha, ha'⟩ := h i
    apply ha
    simpa using DFunLike.congr_fun (linearIndependent_iff.mp hs (Finsupp.single i a) (by simpa)) i

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
s : Set M
inst✝ : Fintype ↑s
⊢ Module.rank R ↥(span R s) ≤ ↑s.toFinset.card

Tactic:
simpa using rank_span_le (R := R) s

Goal state after:
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : x ∈ adjoin R s), p x hx → p (r • x) ⋯
star : ∀ (x : A) (hx : x ∈ adjoin R s), p x hx → p (Star.star x) ⋯
a : A
ha : a ∈ adjoin R s
⊢ p a ha

Tactic:
refine NonUnitalAlgebra.adjoin_induction (fun x hx ↦ ?_) add zero mul smul ha
  push _ ∈ _ at hx
  obtain (hx | hx) := hx
  · exact mem x hx
  · simpa using star _ (NonUnitalAlgebra.subset_adjoin R (by simpa using Or.inl hx)) (mem _ hx)

Goal state after:
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✝¹⁶ : NonUnitalSemiring A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module R A
inst✝¹³ : NonUnitalSemiring B
inst✝¹² : StarRing B
inst✝¹¹ : Module R B
inst✝¹⁰ : FunLike F A B
inst✝⁹ : NonUnitalAlgHomClass F R A B
inst✝⁸ : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst✝⁷ : StarRing R
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
inst✝³ : IsScalarTower R B B
inst✝² : SMulCommClass R B B
inst✝¹ : StarModule R B
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
r : R
⊢ ∀ (x : ↥(iSup K)),
    Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ (r • x) =
      (MonoidHom.id R) r • Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ x

Tactic:
by
        dsimp only [SetLike.coe_sort_coe, NonUnitalAlgHom.coe_comp, Function.comp_apply,
          inclusion_mk, Eq.ndrec, id_eq, eq_mpr_eq_cast]
        apply Set.iUnionLift_unary (coe_iSup_of_directed dir) _ (fun _ x => r • x)
          (fun _ _ => rfl)
        all_goals simp

Goal state after:
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
inst✝ : StrongRankCondition R
v : M
h : ∀ (w : M), ∃ c, c • v = w
⊢ finrank R M ≤ 1

Tactic:
← map_one toNat,

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
v : M
h : ∀ (w : M), ∃ c, c • v = w
⊢ finrank R M ≤ toNat 1
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this✝ : Nontrivial K
κ : Type v
t' : Basis κ K V
h : ∃ p ⊆ range ⇑t', #↑p = c
t : Basis (↑(range ⇑t')) K V := t'.reindexRange
this : LinearIndepOn K id (range ⇑t')
⊢ ∃ s, #↑s = c ∧ LinearIndepOn K id s

Tactic:
rcases h with ⟨s, hst, hsc⟩

Goal state after:
case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this✝ : Nontrivial K
κ : Type v
t' : Basis κ K V
t : Basis (↑(range ⇑t')) K V := t'.reindexRange
this : LinearIndepOn K id (range ⇑t')
s : Set V
hst : s ⊆ range ⇑t'
hsc : #↑s = c
⊢ ∃ s, #↑s = c ∧ LinearIndepOn K id s
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mul_scalar
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
a✝ : FreeAlgebra R X
a b : Pre R X
r✝ s✝ : R
⊢ liftFun R X f (Pre.ofScalar (r✝ * s✝)) = liftFun R X f (Pre.ofScalar r✝ * Pre.ofScalar s✝)

Tactic:
exact (algebraMap R A).map_mul _ _

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
⊢ eval₂ f x (X ^ n) = x ^ n

Tactic:
rw [X_pow_eq_monomial]
  convert! eval₂_monomial f x (n := n) (r := 1)
  simp

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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
l : E →ₛₗ.[σ] F
hl : l ∈ c
x : ↥l.domain
⊢ ↑l x = ↑(LinearPMap.sSup c hc) ⟨↑x, ⋯⟩

Tactic:
apply (Classical.choose_spec (sSup_aux c hc) hl).2

Goal state after:
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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
l : E →ₛₗ.[σ] F
hl : l ∈ c
x : ↥l.domain
⊢ ↑x = ↑⟨↑x, ⋯⟩
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
⊢ Prime n.minFac ↔ n ≠ 1

Tactic:
refine ⟨?_, minFac_prime⟩
  rintro h rfl
  simp only [minFac_one, not_prime_one] at h

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

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

Tactic:
rw [coeff_mul, Finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]
  · rintro ⟨i, j⟩ h1 h2
    rw [coeff_X_pow, if_neg, mul_zero]
    grind [mem_antidiagonal]
  · grind [mem_antidiagonal]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
h✝ : ¬a = 0
⊢ max p.support.max ↑n ≤ max p.degree ↑n

Tactic:
exact le_rfl

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p ≠ 0
h : p.degree < q.degree
⊢ p.natDegree < q.natDegree

Tactic:
by
    have hq : q ≠ 0 := ne_zero_of_degree_gt h
    rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at h

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✝ : AddZeroClass A
hD : Function.Injective D
⊢ Monic D 1

Tactic:
rw [Monic, one_def, leadingCoeff_single hD]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
h : IsUnit p
⊢ p.natDegree = 0

Tactic:
by
  nontriviality R
  obtain ⟨q, hq⟩ := h.exists_right_inv
  have := natDegree_mul (left_ne_zero_of_mul_eq_one hq) (right_ne_zero_of_mul_eq_one hq)
  rw [hq, natDegree_one, eq_comm, add_eq_zero] at this
  exact this.1

Goal state after:
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
p : R[X]
x : A
⊢ (aeval x) p ∈ R[x]

Tactic:
by
  simp [adjoin_singleton_eq_range_aeval]

Goal state after:
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✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p✝ q r✝ : R[X]
r : R
p : A[X]
⊢ ((C.comp (algebraMap R A)) r * p).toFinsupp = (p * (C.comp (algebraMap R A)) r).toFinsupp

Tactic:
by
      dsimp only [RingHom.toFun_eq_coe, RingHom.comp_apply]
      simp_rw [toFinsupp_mul, toFinsupp_C]
      convert! Algebra.commutes' r p.toFinsupp

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
i : ι
inst✝ : NoMaxOrder (β i)
a : Lex ((i : ι) → β i)
b : β i
hb : a i < b
⊢ ∃ b, a < b

Tactic:
classical
    exact ⟨Function.update a i b, i, fun j hj =>
      (Function.update_of_ne hj.ne b a).symm, by rwa [Function.update_self i b]⟩

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

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

Tactic:
simp [X, monomial_pow]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
n : ℕ
⊢ (if 1 = 0 then ∅ else {Finsupp.single s n}) = {Finsupp.single s n}

Tactic:
if_neg (one_ne_zero' R)

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
n : ℕ
⊢ {Finsupp.single s n} = {Finsupp.single s n}
Module: Mathlib.Data.DFinsupp.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt : x < y
⊢ ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

Tactic:
obtain ⟨hle, j, hlt⟩ := Pi.lt_def.1 hlt

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt✝ : x < y
hle : ⇑x ≤ ⇑y
j : ι
hlt : x j < y j
⊢ ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : s ≤ m
⊢ coeff m (p * (monomial s) r) = coeff (m - s) p * r

pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : ¬s ≤ m
⊢ coeff m (p * (monomial s) r) = 0

Tactic:
· conv_rhs => rw [← coeff_mul_monomial _ s]
    rw [tsub_add_cancel_of_le h]

Goal state after:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : ¬s ≤ m
⊢ coeff m (p * (monomial s) r) = 0
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✝ : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
⊢ (∀ (i_1 : σ →₀ ℕ), (if i = i_1 then x else 0) ∈ M) ↔ x ∈ M

Tactic:
exact ⟨fun h ↦ by simpa using h i, fun hs j ↦ by split <;> simp [hs]⟩

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✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
⊢ p ∈ coeffsIn σ M ↔ ↑p.coeffs ⊆ ↑M

Tactic:
by
  simp only [mem_coeffsIn, coeffs, Finset.coe_image, image_subset_iff]
  refine ⟨fun h x _ ↦ h x, fun h i ↦ ?_⟩
  by_cases hp : i ∈ p.support
  · exact h hp
  · convert! M.zero_mem
    simpa using hp

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
⊢ degreeOf n 1 = 0

Tactic:
simp [degreeOf_def, degrees_one]

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

Goal state before:
pp: σ : Type u_1
A : Type u_3
inst✝¹ : CommRing A
inst✝ : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
⊢ (∃ d, coeff d (C a * φ) ≠ 0 ∧ i ∈ d.support) ↔ ∃ d, coeff d φ ≠ 0 ∧ i ∈ d.support

Tactic:
apply exists_congr

Goal state after:
σ : Type u_1
A : Type u_3
inst✝¹ : CommRing A
inst✝ : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
⊢ ∀ (a_1 : σ →₀ ℕ), coeff a_1 (C a * φ) ≠ 0 ∧ i ∈ a_1.support ↔ coeff a_1 φ ≠ 0 ∧ i ∈ a_1.support
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ (X s).totalDegree = 1

Tactic:
totalDegree,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ ((X s).support.sup fun s ↦ s.sum fun x e ↦ e) = 1
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : f.totalDegree < ∑ i ∈ d.support, d i
⊢ coeff d f = 0

Tactic:
totalDegree,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : (f.support.sup fun s ↦ s.sum fun x e ↦ e) < ∑ i ∈ d.support, d i
⊢ coeff d f = 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
⊢ reflect N (C c * X ^ n) = C c * X ^ (revAt N) n

Tactic:
by
  ext
  grind

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0

Tactic:
by_cases! h : #f.support ≤ 1

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support ≤ 1
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0

case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : 1 < #f.support
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
h : f.coeff (f.natDegree - 1) = 0
⊢ f.nextCoeff = 0

Tactic:
simp [nextCoeff_eq_zero, h, eq_zero_or_pos]

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

Goal state before:
pp: 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
⊢ ((X - C x) * P).natDegree = P.natDegree + 1

Tactic:
natDegree_mul (X_sub_C_ne_zero x) hp,

Goal state after:
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
⊢ (X - C x).natDegree + P.natDegree = P.natDegree + 1
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 = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0

pp: case inr
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 ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0

Tactic:
· simp_rw [h, ne_eq, or_true, iff_true, ← Nat.le_zero, ← h, natDegree_map_le]

Goal state after:
case inr
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 ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

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

Tactic:
rw [degree_eq_natDegree hp, degree_eq_natDegree (ne_zero_of_degree_gt hq), ← Nat.cast_mul,
    ← natDegree_comp]

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
⊢ (p.comp q).degree = ↑(p.comp q).natDegree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
⊢ (((optionEquivLeft R S₁) p).coeff i).totalDegree + i ≤ p.totalDegree

Tactic:
totalDegree,

Goal state after:
case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
⊢ ((((optionEquivLeft R S₁) p).coeff i).support.sup fun s ↦ s.sum fun x e ↦ e) + i ≤ p.totalDegree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
⊢ (((optionEquivLeft R S₁) p).coeff i).totalDegree ≤ p.totalDegree

Tactic:
totalDegree,

Goal state after:
case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
⊢ ((((optionEquivLeft R S₁) p).coeff i).support.sup fun s ↦ s.sum fun x e ↦ e) ≤ p.totalDegree
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
⊢ q.leadingCoeff ≠ 0

Tactic:
leadingCoeff_ne_zero

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ q ≠ 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f = 0 ∨ f.leadingCoeff ≠ 0

Tactic:
leadingCoeff_ne_zero

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

Goal state before:
pp: case e'_3
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty
σ : Fin n →₀ ℕ
hσ1 : σ ∈ (((finSuccEquiv R n) f).coeff i).support
hσ2 : ((((finSuccEquiv R n) f).coeff i).support.sup fun s ↦ s.sum fun x e ↦ e) = σ.sum fun x e ↦ e
σ' : Fin (n + 1) →₀ ℕ := cons i σ
⊢ (((finSuccEquiv R n) f).coeff i).totalDegree + i = σ'.sum fun x e ↦ e

Tactic:
totalDegree,

Goal state after:
case e'_3
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty
σ : Fin n →₀ ℕ
hσ1 : σ ∈ (((finSuccEquiv R n) f).coeff i).support
hσ2 : ((((finSuccEquiv R n) f).coeff i).support.sup fun s ↦ s.sum fun x e ↦ e) = σ.sum fun x e ↦ e
σ' : Fin (n + 1) →₀ ℕ := cons i σ
⊢ ((((finSuccEquiv R n) f).coeff i).support.sup fun s ↦ s.sum fun x e ↦ e) + i = σ'.sum fun x e ↦ e
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
⊢ h.unit⁻¹ • p.leadingCoeff = 1

Tactic:
Units.smul_def

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
⊢ ↑h.unit⁻¹ • p.leadingCoeff = 1
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ Function.RightInverse (fun p ↦ ⟨X ^ n + ↑p, ⋯⟩) fun p ↦ ⟨(↑p).eraseLead, ⋯⟩

Tactic:
rintro ⟨p, hp⟩

Goal state after:
R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
⊢ (fun p ↦ ⟨(↑p).eraseLead, ⋯⟩) ((fun p ↦ ⟨X ^ n + ↑p, ⋯⟩) ⟨p, hp⟩) = ⟨p, hp⟩
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : p = 0
⊢ False

Tactic:
rw [hp_zero, degree_zero] at h
    rcases hs with ⟨x, hx⟩
    exact not_lt_bot (h x hx)

Goal state after: