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

Goal state before:
pp: F : Type v'
R : Type u
A : Type v
B : Type w
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : StarRing 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
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
f : F
⊢ ↑(map f ⊥) = ↑⊥

Tactic:
simp [NonUnitalStarSubalgebra.coe_map]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ finrank R M = 0 ↔ ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0

Tactic:
by
  rw [← rank_eq_zero_iff (R := R), ← finrank_eq_rank]
  norm_cast

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)
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ 0 = 0

Tactic:
by
        dsimp only [SetLike.coe_sort_coe, NonUnitalAlgHom.coe_comp, Function.comp_apply,
          inclusion_mk, Eq.ndrec, id_eq, eq_mpr_eq_cast]
        exact Set.iUnionLift_const _ (fun i : ι => (0 : K i)) (fun _ => rfl) _ (by simp)

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

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
⊢ finrank K V = 1 ↔ ∃ v, v ≠ 0 ∧ ∀ (w : V), ∃ c, c • v = w

Tactic:
by
  rw [← rank_eq_one_iff]
  exact toNat_eq_iff one_ne_zero

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case add_assoc
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 a✝ b✝ c✝ : Pre R X
⊢ liftFun R X f a✝ + liftFun R X f b✝ + liftFun R X f c✝ = liftFun R X f a✝ + (liftFun R X f b✝ + liftFun R X f c✝)

Tactic:
add_assoc

Goal state after:
case add_assoc
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 a✝ b✝ c✝ : Pre R X
⊢ liftFun R X f a✝ + (liftFun R X f b✝ + liftFun R X f c✝) = liftFun R X f a✝ + (liftFun R X f b✝ + liftFun R X f c✝)
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case h
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 g : E →ₛₗ.[σ] F
x : E
⊢ x ∈ (f + g).domain ↔ x ∈ (g + f).domain

pp: case h'
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 g : E →ₛₗ.[σ] F
x : E
y : x ∈ (f + g).domain
hxy : x ∈ (g + f).domain
⊢ ↑(f + g) ⟨x, y⟩ = ↑(g + f) ⟨x, hxy⟩

Tactic:
· simp only [add_domain, inf_comm]

Goal state after:
case h'
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 g : E →ₛₗ.[σ] F
x : E
y : x ∈ (f + g).domain
hxy : x ∈ (g + f).domain
⊢ ↑(f + g) ⟨x, y⟩ = ↑(g + f) ⟨x, hxy⟩
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p : R[X]
S : Type u_1
inst✝ : Ring S
f : R →+* S
x : S
⊢ eval₂ f x 0 = 0

Tactic:
eval₂_zero

Goal state after:
R : Type u
inst✝¹ : Ring R
p : R[X]
S : Type u_1
inst✝ : Ring S
f : R →+* S
x : S
⊢ 0 = 0
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: ⊢ decidablePrime = decidablePrime'

Tactic:
by
  subsingleton

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hp : ExpChar R p
hq : ExpChar R q
⊢ p = q

Tactic:
rcases hp with ⟨hp⟩ | ⟨hp'⟩

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

case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hq : ExpChar R q
hp' : Nat.Prime p
hchar✝ : CharP R p
⊢ p = q
Module: Mathlib.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 : E →ₗ.[R] F
y : F
⊢ y ∈ Set.range ↑f ↔ ∃ x, (x, y) ∈ f.graph

Tactic:
constructor <;> intro h
  · rw [Set.mem_range] at h
    rcases h with ⟨⟨x, hx⟩, h⟩
    use x
    rw [← h]
    exact f.mem_graph ⟨x, hx⟩
  grind

Goal state after:
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 : E →ₗ.[R] F
y : F
⊢ y ∈ Set.range ↑f ↔ ∃ x, (x, y) ∈ f.graph

Tactic:
by
  constructor <;> intro h
  · rw [Set.mem_range] at h
    rcases h with ⟨⟨x, hx⟩, h⟩
    use x
    rw [← h]
    exact f.mem_graph ⟨x, hx⟩
  grind

Goal state after:
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 : E →ₗ.[R] F
⊢ (Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph).toLinearPMap.domain = f.toFun.range

Tactic:
Submodule.toLinearPMap_domain,

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 : E →ₗ.[R] F
⊢ Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph) = f.toFun.range
Module: Mathlib.Algebra.Polynomial.Coeff

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

Tactic:
by
  rcases p with ⟨⟩
  rcases q with ⟨⟩
  simp_rw [← ofFinsupp_add, coeff]
  exact Finsupp.add_apply _ _ _

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

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

Tactic:
let ⟨n, hn⟩ := not_forall.1 (mt Option.eq_none_iff_forall_not_mem.2 (mt degree_eq_bot.1 hp))

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
hn : ¬n ∉ p.degree
⊢ p.degree = ↑p.natDegree
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✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
⊢ supDegree D (∑ i ∈ s, f i) ≤ s.sup fun i ↦ supDegree D (f i)

Tactic:
by
  classical
  simp only [supDegree, coeff_sum]
  grw [Finsupp.support_finsetSum, Finset.sup_biUnion]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
this : DecidableEq R := Classical.decEq R
h : a = 0
⊢ ((monomial n) a).degree ≤ ↑n

Tactic:
rw [h, (monomial n).map_zero, degree_zero]; exact bot_le

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
⊢ C r ∣ φ ↔ ∀ (i : ℕ), r ∣ φ.coeff i

Tactic:
constructor
  · rintro ⟨φ, rfl⟩ c
    rw [coeff_C_mul]
    apply dvd_mul_right
  · intro h
    choose c hc using h
    classical
      let c' : ℕ → R := fun i => if i ∈ φ.support then c i else 0
      let ψ : R[X] := ∑ i ∈ φ.support, monomial i (c' i)
      use ψ
      ext i
      simp only [c', ψ, coeff_C_mul, mem_support_iff, coeff_monomial, finsetSum_coeff,
        Finset.sum_ite_eq']
      split_ifs with hi
      · rw [hc]
      · rw [Classical.not_not] at hi
        rwa [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]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
hp : ¬p = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
by rwa [hq.leadingCoeff, mul_one, Ne, leadingCoeff_eq_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.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Tactic:
by
  simp [← coeff_natDegree, natDegree_mul' h, coeff_mul_degree_add_degree]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
hp : p ≠ 0
⊢ (X * p).natDegree = p.natDegree + 1

Tactic:
rw [commute_X p, natDegree_mul_X hp]

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι✝ : Type y
a b : R✝
m n✝ : ℕ
inst✝³ : Semiring R✝
p✝ q✝ r : R✝[X]
inst✝² : Semiring S
f : R✝ →+* S
ι : Type ?u.38
inst✝¹ : Finite ι
R : ι → Type u_1
inst✝ : (i : ι) → Semiring (R i)
p q : ((i : ι) → R i)[X]
h : (RingHom.pi fun i ↦ mapRingHom (Pi.evalRingHom R i)) p = (RingHom.pi fun i ↦ mapRingHom (Pi.evalRingHom R i)) q
n : ℕ
i : ι
⊢ p.coeff n i = q.coeff n i

Tactic:
simpa using congr_arg (fun p ↦ coeff (p i) n) h

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
p : S[X]
⊢ ∀ (p q : S[X]), (∃ a, map f a = p) → (∃ a, map f a = q) → ∃ a, map f a = p + q

Tactic:
rintro _ _ ⟨p, rfl⟩ ⟨q, rfl⟩

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
p✝ : S[X]
p q : R[X]
⊢ ∃ a, map f a = map f p + map f q
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
⊢ b ≠ p.natDegree → (fun a b ↦ (C b * q ^ a).coeff (p.natDegree * q.natDegree)) b (p.coeff b) = 0

Tactic:
hbp

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ (fun a b ↦ (C b * q ^ a).coeff (p.natDegree * q.natDegree)) b (p.coeff b) = 0
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : p.Monic
hfp : map f p = 0
x : R
⊢ f x * (map f p).coeff p.natDegree = 0

Tactic:
simp only [hfp, mul_zero, coeff_zero]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
x : S
⊢ (aeval x) p = ∑ i ∈ range (p.natDegree + 1), p.coeff i • x ^ i

Tactic:
by
  simp_rw [Algebra.smul_def]
  exact eval₂_eq_sum_range (algebraMap R S) x

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

Goal state before:
pp: case pos
S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ (RingHom.id S) (f.coeff i) * z ^ i + ∑ x ∈ f.support.erase i, (RingHom.id S) (f.coeff x) * z ^ x
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
⊢ p ∣ f.coeff i * z ^ i

Tactic:
refine (dvd_add_left ?_).mp dvd_eval

Goal state after:
case pos
S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ (RingHom.id S) (f.coeff i) * z ^ i + ∑ x ∈ f.support.erase i, (RingHom.id S) (f.coeff x) * z ^ x
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
⊢ p ∣ ∑ x ∈ f.support.erase i, (RingHom.id S) (f.coeff x) * z ^ x
Module: Mathlib.Algebra.MvPolynomial.Eval

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

Tactic:
change _ = eval₂Hom f g (eval₂ C q p)

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
⊢ eval₂ f (fun t ↦ eval₂ f g (q t)) p = (eval₂Hom f g) (eval₂ C q p)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case e'_4
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i f.degrees + Multiset.count i g.degrees = Multiset.count i (f.degrees + g.degrees)

Tactic:
Multiset.count_add

Goal state after:
case e'_4
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i f.degrees + Multiset.count i g.degrees = Multiset.count i f.degrees + Multiset.count i g.degrees
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x : MvPolynomial R ℤ
n : ℤ
⊢ eval₂ c (⇑f ∘ X) (C n) = f (C n)

Tactic:
rw [hom_C f, eval₂_C]

Goal state after:
S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x : MvPolynomial R ℤ
n : ℤ
⊢ c n = ↑n
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
⊢ cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0

Tactic:
by
  refine ⟨fun h => ?_, fun h => h.casesOn cons_ne_zero_of_left cons_ne_zero_of_right⟩
  refine imp_iff_not_or.1 fun h' c => h ?_
  rw [h', c, Finsupp.cons_zero_zero]

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

Goal state before:
pp: R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
d : σ →₀ ℕ
hd : d ∈ φ.support
i : σ
hi : i ∈ d.support
hgi : g i = 0
⊢ (eval₂Hom f g) ((monomial d) (coeff d φ)) = 0

Tactic:
eval₂Hom_monomial,

Goal state after:
R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
d : σ →₀ ℕ
hd : d ∈ φ.support
i : σ
hi : i ∈ d.support
hgi : g i = 0
⊢ (f (coeff d φ) * d.prod fun i k ↦ g i ^ k) = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * X i ^ k) = degreeOf i p + k
this : p * X i ^ k ≠ 0
⊢ degreeOf i p + k + 1 = degreeOf i p + (k + 1)

Tactic:
add_assoc

Goal state after:
case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * X i ^ k) = degreeOf i p + k
this : p * X i ^ k ≠ 0
⊢ degreeOf i p + (k + 1) = degreeOf i p + (k + 1)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
h : p.coeff 0 = 0
hlt : p.degree ≤ 0
this : p = 0
⊢ False

Tactic:
exact hp this

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

Goal state before:
pp: case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ p.natTrailingDegree + n ≤ (p * X ^ n).natTrailingDegree

Tactic:
rw [natTrailingDegree_eq_support_min' fun h => hp (mul_X_pow_eq_zero h), Finset.le_min'_iff]

Goal state after:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ ∀ y ∈ (p * X ^ n).support, p.natTrailingDegree + n ≤ y
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = 0 → motive f
hf : #f.support = 0 + 1
⊢ motive (f.eraseLead + C f.leadingCoeff * X ^ f.natDegree)

pp: case succ.succ
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ motive (f.eraseLead + C f.leadingCoeff * X ^ f.natDegree)

Tactic:
· convert C_mul_pow f.natDegree f.leadingCoeff ?_ df
      · convert! zero_add (C (leadingCoeff f) * X ^ f.natDegree)
        rw [← card_support_eq_zero, card_support_eraseLead' hf]
      · rw [leadingCoeff_ne_zero, Ne, ← card_support_eq_zero, hf]
        exact zero_ne_one.symm

Goal state after:
case succ.succ
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ motive (f.eraseLead + C f.leadingCoeff * X ^ f.natDegree)
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q ≠ 0
⊢ (p * q).natDegree = p.natDegree + q.natDegree

Tactic:
rw [natDegree_mul']
  simpa [hp.leadingCoeff, leadingCoeff_ne_zero]

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

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
l : List S[X]
⊢ l.sum.natDegree ≤ List.foldr max 0 (List.map natDegree l)

Tactic:
by
  apply List.sum_le_foldr_max natDegree
  · simp
  · exact natDegree_add_le

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

Goal state before:
pp: case neg
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
i : ι
hi : i ∈ s
hf : ¬f i = 0
⊢ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).coeff (f i).natDegree ≠ 0

Tactic:
rw [finsetSum_coeff]

Goal state after:
case neg
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
i : ι
hi : i ∈ s
hf : ¬f i = 0
⊢ ∑ b ∈ s, (v b • map (algebraMap R A) (f b)).coeff (f i).natDegree ≠ 0
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case inl
x y n : ℕ
h : y ≤ x
⊢ x - y ∣ x ^ n - y ^ n

pp: case inr
x y n : ℕ
h : x < y
⊢ x - y ∣ x ^ n - y ^ n

Tactic:
· have : y ^ n ≤ x ^ n := Nat.pow_le_pow_left h _
    exact mod_cast sub_dvd_pow_sub_pow (x : ℤ) (↑y) n

Goal state after:
case inr
x y n : ℕ
h : x < y
⊢ x - y ∣ x ^ n - y ^ n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
n : ℕ
h✝ : Submodule.span R s ≤ degreeLE R ↑n
⊢ Submodule.span R s ≤ degreeLT R (n + 1)

Tactic:
by rwa [degreeLT_succ_eq_degreeLE]

Goal state after:
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this✝ :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a ↦ a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (l2.sum fun i a ↦ a • _root_.id i) = ↑(l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    (Finsupp.linearCombination R v) l = l.sum fun i a ↦ a • v i
⊢ ↑(l z) * _root_.id z ∈ span R (p * q)

Tactic:
← hl,

Goal state after:
case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this✝ :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a ↦ a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (l2.sum fun i a ↦ a • _root_.id i) = ↑(l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    (Finsupp.linearCombination R v) l = l.sum fun i a ↦ a • v i
⊢ (l2.sum fun i a ↦ a • _root_.id i) * _root_.id z ∈ span R (p * q)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
i : ℕ
⊢ p.restriction.coeff i = 0 ↔ p.coeff i = 0

Tactic:
conv_rhs => rw [← coeff_restriction]

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
i : ℕ
⊢ p.restriction.coeff i = 0 ↔ ↑(p.restriction.coeff i) = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case inl
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hi : i < m
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P

Tactic:
rw [mul_comm]
          apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hf hi)

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
⊢ FiniteType S A

Tactic:
obtain ⟨s, hS⟩ := hA.out

Goal state after:
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 = ⊤
⊢ FiniteType S A
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
⊢ FiniteType R (FreeAlgebra S ι)

Tactic:
cases nonempty_fintype ι
  refine .trans ‹_› ⟨Finset.univ.image (FreeAlgebra.ι _), ?_⟩
  rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
  exact FreeAlgebra.adjoin_range_ι ..

Goal state after: