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

Goal state before:
pp: ι : Type w
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i // V i ≠ ⊥ }
i : I
⊢ ∃ v ∈ V ↑i, v ≠ 0

Tactic:
rw [← Submodule.ne_bot_iff]

Goal state after:
ι : Type w
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i // V i ≠ ⊥ }
i : I
⊢ V ↑i ≠ ⊥
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
W : Submodule K V
w : V
left✝ : w ∈ W
hw : w ≠ 0
⊢ IsAtom (K ∙ w)

Tactic:
exact nonzero_span_atom w hw

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✝¹¹ : 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
s : Set A
hs : s = ↑S
x : A
hx : x ∈ ↑S
⊢ star x ∈ ↑S

Tactic:
exact S.star_mem' hx

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

Goal state before:
pp: case mp.inr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
κ : Type v
b : Basis κ K V
hd : Subsingleton κ
i : κ
⊢ ∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v

Tactic:
· use b i
      have h' : K ∙ b i = ⊤ :=
        (subsingleton_range b).eq_singleton_of_mem (mem_range_self i) ▸ b.span_eq
      intro v
      have hv : v ∈ (⊤ : Submodule K V) := mem_top
      rwa [← h', mem_span_singleton] at hv

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
x✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) 0) * a✝) = 0

Tactic:
rw [map_zero]

Goal state after:
case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
x✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) (Pre.ofScalar 0 * a✝) = 0
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : FreeAlgebra R X →ₐ[R] A
⊢ (lift R) (⇑g ∘ ι R) = g

Tactic:
rw [← lift_symm_apply]

Goal state after:
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : FreeAlgebra R X →ₐ[R] A
⊢ (lift R) ((lift R).symm g) = g
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

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

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case refine_1
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
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ ∃ x, (a, x) ∈ g

Tactic:
convert! ha

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
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ (∃ x, (a, x) ∈ g) ↔ a ∈ map (LinearMap.fst R E F) g
Module: Mathlib.Algebra.Polynomial.Coeff

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

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
⊢ (p * X ^ n).coeff d = 0

Tactic:
· rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
⊢ (p * X ^ n).coeff d = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

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

Tactic:
rw [List.map_replicate]

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

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ ¬p.support = ∅

Tactic:
support_eq_empty

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ ¬p = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : (p ^ n).natDegree ≤ n * p.natDegree
⊢ (p ^ (n + 1)).natDegree ≤ (n + 1) * p.natDegree

Tactic:
grw [pow_succ, Nat.succ_mul, natDegree_mul_le, ih]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h1 : p ∣ q
h2 : q ≠ 0
⊢ p.natDegree ≤ q.natDegree

Tactic:
by
  obtain ⟨q, rfl⟩ := h1
  rw [mul_ne_zero_iff] at h2
  rw [natDegree_mul h2.1 h2.2]; exact Nat.le_add_right _ _

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 ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
hn0 : ¬n = 0
⊢ (p ^ n).natDegree = n * p.natDegree

Tactic:
rw [hp0, zero_pow hn0]; simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
a : R
⊢ (X + C a).degree = 1

Tactic:
have : degree (C a) < degree (X : R[X]) :=
    calc
      degree (C a) ≤ 0 := degree_C_le
      _ < 1 := WithBot.coe_lt_coe.mpr zero_lt_one
      _ = degree X := degree_X.symm
  rw [degree_add_eq_left_of_degree_lt this, degree_X]

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

Goal state before:
pp: R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ 0 < (X ^ n).degree

Tactic:
rwa [degree_X_pow, Nat.cast_pos]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
i j : ℕ
⊢ (monomial i) 1 = (monomial j) 1 ↔ i = j

Tactic:
simp_rw [← ofFinsupp_single, ofFinsupp.injEq]

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
i j : ℕ
⊢ AddMonoidAlgebra.single i 1 = AddMonoidAlgebra.single j 1 ↔ i = j
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
x✝ : R[X]
⊢ ((aeval p).comp (aeval q)) x✝ = (AlgHom.id R R[X]) x✝

Tactic:
simp [← comp_eq_aeval, comp_assoc, hpq, hqp]

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✝³ : 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
x✝ : R[X]
⊢ ((aeval q).comp (aeval p)) x✝ = (AlgHom.id R R[X]) x✝

Tactic:
simp [← comp_eq_aeval, comp_assoc, hpq, hqp]

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✝ : ∀ (i : ι), Std.Trichotomous s
wf : WellFounded r
a b : (i : ι) → β i
hab : ¬Pi.Lex r s a b
hba : ¬Pi.Lex r s b a
⊢ a = b

Tactic:
by_contra! h

Goal state after:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), Std.Trichotomous s
wf : WellFounded r
a b : (i : ι) → β i
hab : ¬Pi.Lex r s a b
hba : ¬Pi.Lex r s b a
h : a ≠ b
⊢ False
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
⊢ ∃ a, a ≠ 0 ∧ a • P = 0

Tactic:
by_contra! h

Goal state after:
R : Type u
inst✝ : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
h : ∀ (a : R), a ≠ 0 → a • P ≠ 0
⊢ False
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
hp : eval₂ f g p = 0
⊢ eval₂ f g (p * q) = 0

Tactic:
simp [eval₂_mul f g, hp]

Goal state after:
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
  classical
  have : (x.neLocus y : Set ι).WellFoundedOn r := (x.neLocus y).finite_toSet.wellFoundedOn
  obtain ⟨i, hi, hl⟩ := this.has_min { i | x i < y i } ⟨⟨j, mem_neLocus.2 hlt.ne⟩, hlt⟩
  refine ⟨i, fun k hk ↦ ⟨hle k, ?_⟩, hi⟩
  exact of_not_not fun h ↦ hl ⟨k, mem_neLocus.2 (ne_of_not_le h).symm⟩ ((hle k).lt_of_not_ge h) hk

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ¬p.support = ∅ ↔ p ≠ 0

Tactic:
support_eq_empty

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ¬p = 0 ↔ p ≠ 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
p : MvPolynomial σ S
i : σ →₀ ℕ
⊢ (monomial i) 1 * p ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

Tactic:
simp [mul_comm]

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
s : σ
⊢ X s * p ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

Tactic:
simp [mul_comm]

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:
by
  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.Rename

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ constantCoeff ((rename f) φ) = constantCoeff φ

Tactic:
apply φ.induction_on
  · intro a
    simp only [constantCoeff_C, rename_C]
  · intro p q hp hq
    simp only [hp, hq, map_add]
  · intro p n hp
    simp only [hp, rename_X, constantCoeff_X, map_mul]

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
i : Fin (n + 1)
hi : i ∈ (cons y s).support
⊢ ∀ (a : Fin n), i = a.succ → ¬s a = 0 ∧ a.succ = i

Tactic:
rintro i rfl

Goal state after:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
i : Fin n
hi : i.succ ∈ (cons y s).support
⊢ ¬s i = 0 ∧ i.succ = i.succ
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m ↦ (toMultiset m).card) = (toMultiset b).card
h : b ∈ q.support
⊢ p.totalDegree ≤ q.totalDegree

Tactic:
rw [totalDegree_eq p, hb₂, totalDegree_eq]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m ↦ (toMultiset m).card) = (toMultiset b).card
h : b ∈ q.support
⊢ (toMultiset b).card ≤ q.support.sup fun m ↦ (toMultiset m).card
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : a * ai = 1
⊢ p.natDegree = (p * 1).natDegree

Tactic:
nth_rw 1 [← mul_one p]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
f : MvPolynomial σ R
φ : R →+* S
a : σ → S
⊢ Polynomial.eval₂ φ (a default) ((uniqueAlgEquiv R σ) f) = eval₂ φ a f

Tactic:
by
  simp only [MvPolynomial.uniqueAlgEquiv_apply]
  induction f using MvPolynomial.induction_on' with
  | monomial d r =>
    rw [← MvPolynomial.uniqueAlgEquiv_apply (R := R) (σ := σ), uniqueAlgEquiv_monomial]
    simp only [Polynomial.eval₂_monomial, eval₂_monomial]
    rw [Finsupp.unique_single d, Finsupp.prod_single_index]
    · simp
    · simp only [pow_zero]
  | add f g hf hg => simp only [eval₂_add, Polynomial.eval₂_add, hf, hg]

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

Goal state before:
pp: case neg.inl.zero
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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
hn₂ : n = 0
⊢ ((X - C x) * (monomial P.natDegree) P.leadingCoeff).coeff 0 = 0

pp: case neg.inl.succ
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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
n✝ : ℕ
hn₂ : n = n✝ + 1
⊢ ((X - C x) * (monomial P.natDegree) P.leadingCoeff).coeff (n✝ + 1) = 0

Tactic:
· simpa [coeff_monomial, hp] using! fun _ ↦ by lia

Goal state after:
case neg.inl.succ
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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
n✝ : ℕ
hn₂ : n = n✝ + 1
⊢ ((X - C x) * (monomial P.natDegree) P.leadingCoeff).coeff (n✝ + 1) = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
⊢ ¬(((finSuccEquiv R n) f).coeff i).support = ∅

Tactic:
support_eq_empty

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
⊢ ¬((finSuccEquiv R n) f).coeff i = 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0
⊢ t.prod.natDegree = (Multiset.map (fun f ↦ f.natDegree) t).sum

Tactic:
revert h
  refine Multiset.induction_on t ?_ fun a t ih ht => ?_; · simp
  rw [Multiset.map_cons, Multiset.prod_cons] at ht ⊢
  rw [Multiset.sum_cons, Polynomial.natDegree_mul', ih]
  · apply right_ne_zero_of_mul ht
  · rwa [Polynomial.leadingCoeff_multiset_prod']
    apply right_ne_zero_of_mul ht

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

Goal state before:
pp: case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsRightRegular p

Tactic:
· intro q r h
    simp only at h
    rw [← sub_eq_zero, ← hp.mul_left_eq_zero_iff, sub_mul, h, sub_self]

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

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

Tactic:
by simpa using geom_sum_mul_neg (op x) n

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
⊢ ∃ p' ∈ s, p.degree ≤ p'.degree

Tactic:
by_contra! h

Goal state after:
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
⊢ False
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ⊤.FG
s : Finset A
hs : span R ↑s = ⊤
⊢ ↑s ⊆ ↑(toSubmodule (Algebra.adjoin R ↑s))

Tactic:
exact Algebra.subset_adjoin

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
p : Ideal R
x : R
⊢ x ∈ p → x ∈ (map C p).leadingCoeff

Tactic:
intro hx
    exact ((map C p).mem_leadingCoeff x).2 ⟨C x, mem_map_of_mem C hx, leadingCoeff_C x⟩

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

Goal state before:
pp: case mp
R : Type u
inst✝ : CommRing R
P : Ideal R
⊢ (map C P).IsPrime → P.IsPrime

Tactic:
intro H
    have := comap_isPrime C (map C P)
    convert! this using 1
    ext x
    simp only [mem_comap, mem_map_C_iff]
    constructor
    · rintro h (- | n)
      · rwa [coeff_C_zero]
      · simp only [coeff_C_of_ne_zero (Nat.succ_ne_zero _), Submodule.zero_mem]
    · intro h
      simpa only [coeff_C_zero] using h 0

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
hA : FiniteType R A
s : Finset A
hS : adjoin R ↑s = ⊤
b : A
⊢ ↑s ⊆ ↑(adjoin S ↑s)

Tactic:
exact Algebra.subset_adjoin

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

Goal state before:
pp: case pos
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * X ^ (k - q.natDegree)).leadingCoeff
this : (p - q * X ^ (k - q.natDegree)).degree < ↑p.natDegree
hpq : p - q * X ^ (k - q.natDegree) = 0
⊢ p - q * X ^ (k - q.natDegree) ∈ Ideal.span ↑s

Tactic:
rw [hpq]

Goal state after:
case pos
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * X ^ (k - q.natDegree)).leadingCoeff
this : (p - q * X ^ (k - q.natDegree)).degree < ↑p.natDegree
hpq : p - q * X ^ (k - q.natDegree) = 0
⊢ 0 ∈ Ideal.span ↑s
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
this : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : span R (Set.range mj) = ⊤
⊢ n = 0

Tactic:
← surjective_piEquiv_apply_iff

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
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
⊢ n = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case neg
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * X ^ (k - q.natDegree)).leadingCoeff
this : ↑(p - q * X ^ (k - q.natDegree)).natDegree < ↑p.natDegree
hpq : ¬p - q * X ^ (k - q.natDegree) = 0
⊢ (p - q * X ^ (k - q.natDegree)).natDegree < k

Tactic:
Nat.cast_lt,

Goal state after:
case neg
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * X ^ (k - q.natDegree)).leadingCoeff
this : (p - q * X ^ (k - q.natDegree)).natDegree < p.natDegree
hpq : ¬p - q * X ^ (k - q.natDegree) = 0
⊢ (p - q * X ^ (k - q.natDegree)).natDegree < k
Module: Mathlib.GroupTheory.GroupAction.Ring

Goal state before:
pp: case succ
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : R
n : ℕ
ih : (n • x) • y = n • x • y
⊢ (n • x + x) • y = n • x • y + x • y

Tactic:
← ih,

Goal state after:
case succ
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : R
n : ℕ
ih : (n • x) • y = n • x • y
⊢ (n • x + x) • y = (n • x) • y + x • y