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

Goal state before:
pp: α : Type u_1
β : Type u_2
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
b : β
this✝ : Add α := e.add
this : Mul α := e.mul
⊢ Sort ?u.14

Tactic:
exact (ringEquiv e).symm b = e.symm b

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

Goal state before:
pp: case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∈ σ a
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)

Tactic:
rw [mem_iff] at h
    simp only [resolvent, Algebra.algebraMap_eq_smul_one] at *
    rw [smul_assoc, ← smul_sub]
    have h' : ¬IsUnit (r⁻¹ • (s • (1 : A) - a)) := fun hu =>
      h (by simpa only [smul_inv_smul] using IsUnit.smul r hu)
    simp only [Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ h', smul_zero]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid R
inst✝³ : NonUnitalSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x y z : Unitization R A
⊢ (x * y * z).toProd.2 = (x * (y * z)).toProd.2

Tactic:
simp only [snd_mul, fst_mul, smul_add, smul_smul, add_mul, smul_mul_assoc, mul_assoc, mul_add,
        mul_smul_comm, mul_comm z.fst x.fst, mul_comm z.fst y.fst]

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid R
inst✝³ : NonUnitalSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x y z : Unitization R A
⊢ (x.toProd.1 * y.toProd.1) • z.toProd.2 +
        ((x.toProd.1 * z.toProd.1) • y.toProd.2 + (y.toProd.1 * z.toProd.1) • x.toProd.2 +
          z.toProd.1 • (x.toProd.2 * y.toProd.2)) +
      (x.toProd.1 • (y.toProd.2 * z.toProd.2) + y.toProd.1 • (x.toProd.2 * z.toProd.2) +
        x.toProd.2 * (y.toProd.2 * z.toProd.2)) =
    (x.toProd.1 * y.toProd.1) • z.toProd.2 + (x.toProd.1 * z.toProd.1) • y.toProd.2 +
          x.toProd.1 • (y.toProd.2 * z.toProd.2) +
        (y.toProd.1 * z.toProd.1) • x.toProd.2 +
      (y.toProd.1 • (x.toProd.2 * z.toProd.2) + z.toProd.1 • (x.toProd.2 * y.toProd.2) +
        x.toProd.2 * (y.toProd.2 * z.toProd.2))
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁴ : Semiring R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module R A
inst✝⁵ : StarModule R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : IsDomain R
inst✝¹ : IsCancelAdd A
inst✝ : Module.IsTorsionFree R A
r : R
hr : 0 < r
a b : A
hab : a < b
⊢ r • a < r • b

Tactic:
rw [StarOrderedRing.pos_iff] at hr

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹⁴ : Semiring R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module R A
inst✝⁵ : StarModule R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : IsDomain R
inst✝¹ : IsCancelAdd A
inst✝ : Module.IsTorsionFree R A
r : R
hr : r ≠ 0 ∧ r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a b : A
hab : a < b
⊢ r • a < r • b
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
ι : Type w
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
hst : Disjoint s t
⊢ LinearIndepOn R (⇑(span R (f '' s)).mkQ ∘ f) t ↔ LinearIndepOn R f (s ∪ t)

Tactic:
rw [linearIndepOn_union_iff_quotient hst, and_iff_right hs]

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

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Nontrivial R
⊢ lift.{v', v} (Module.rank R M) + lift.{v, v'} (Module.rank R M') ≤ Module.rank R (M × M')

Tactic:
← rank_ulift,

Goal state after:
R : Type u
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Nontrivial R
⊢ Module.rank R (ULift.{v', v} M) + lift.{v, v'} (Module.rank R M') ≤ Module.rank R (M × M')
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: 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
inst✝ : Module.Free R A
⊢ centralizer R ↑includeRight.range = (Algebra.TensorProduct.map (AlgHom.id R A) (center R B).val).range

Tactic:
rw [← centralizer_univ, ← Algebra.coe_top (R := R) (A := B),
    ← centralizer_coe_map_includeRight_eq_center_tensorProduct R A B ⊤]
  ext
  simp [includeRight]

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

Goal state before:
pp: R : Type u
η : Type u₁'
inst✝² : Semiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype η
⊢ Module.rank R (η → R) = ↑(Fintype.card η)

Tactic:
rw [rank_fun_eq_lift_mul, rank_self, Cardinal.lift_one, mul_one]

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

Tactic:
nontriviality R
  constructor
  · contrapose!
    rintro ⟨x, hx⟩
    rw [← Cardinal.one_le_iff_ne_zero]
    have : LinearIndependent R (fun _ : Unit ↦ x) :=
      linearIndependent_iff.mpr (fun l hl ↦ Finsupp.unique_ext <| not_not.mp fun H ↦
        hx _ H ((Finsupp.linearCombination_unique _ _ _).symm.trans hl))
    simpa using this.cardinal_lift_le_rank
  · 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.Basis.VectorSpace

Goal state before:
pp: K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : V
hfv : f v ≠ 0
b₁ : Basis (↑(Basis.ofVectorSpaceIndex K ↥f.ker)) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
i : ↑n := ⟨v, ⋯⟩
hi : b i = v
⊢ f = f v • b.coord i

Tactic:
rw [← hi]

Goal state after:
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : V
hfv : f v ≠ 0
b₁ : Basis (↑(Basis.ofVectorSpaceIndex K ↥f.ker)) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
i : ↑n := ⟨v, ⋯⟩
hi : b i = v
⊢ f = f (b i) • b.coord i
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
K : Type u_7
L : Type u_8
E : Type u_9
F : Type u_10
inst✝⁵ : DivisionRing K
inst✝⁴ : DivisionRing L
σ : K →+* L
inst✝³ : AddCommGroup E
inst✝² : Module K E
inst✝¹ : AddCommGroup F
inst✝ : Module L F
x : E
y : F
hx : x ≠ 0
c : K
hc✝ : c • x = 0
hc : c = 0
⊢ σ c • y = 0

Tactic:
hc,

Goal state after:
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
K : Type u_7
L : Type u_8
E : Type u_9
F : Type u_10
inst✝⁵ : DivisionRing K
inst✝⁴ : DivisionRing L
σ : K →+* L
inst✝³ : AddCommGroup E
inst✝² : Module K E
inst✝¹ : AddCommGroup F
inst✝ : Module L F
x : E
y : F
hx : x ≠ 0
c : K
hc✝ : c • x = 0
hc : c = 0
⊢ σ 0 • y = 0
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case w.refine_1
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
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
⊢ ∀ (x y : ↥(f.domain ⊔ g.domain)), fg (x + y) = fg x + fg y

pp: case w.refine_2
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
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
⊢ ∀ (m : R) (x : ↥(f.domain ⊔ g.domain)), fg (m • x) = σ m • fg x

Tactic:
· rintro ⟨z₁, hz₁⟩ ⟨z₂, hz₂⟩
    rw [← add_assoc, add_right_comm (f _), ← map_add, add_assoc, ← map_add]
    apply fg_eq
    simp only [coe_add, ← add_assoc]
    rw [add_right_comm (x _), hxy, add_assoc, hxy, coe_mk, coe_mk]

Goal state after:
case w.refine_2
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
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
⊢ ∀ (m : R) (x : ↥(f.domain ⊔ g.domain)), fg (m • x) = σ m • fg x
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
W : Type u_1
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Module A V
inst✝³ : AddCommGroup W
inst✝² : Module K W
inst✝¹ : Module A W
inst✝ : LinearMap.CompatibleSMul V W K A
h : finrank K W = 1
f : V →ₗ[A] W
w : f ≠ 0
v : V
n : f v ≠ 0 v
z : W
⊢ ∃ a, (↑K f) a = z

Tactic:
obtain ⟨c, rfl⟩ := (finrank_eq_one_iff_of_nonzero' (f v) n).mp h z

Goal state after:
K : Type u
V : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
W : Type u_1
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Module A V
inst✝³ : AddCommGroup W
inst✝² : Module K W
inst✝¹ : Module A W
inst✝ : LinearMap.CompatibleSMul V W K A
h : finrank K W = 1
f : V →ₗ[A] W
w : f ≠ 0
v : V
n : f v ≠ 0 v
c : K
⊢ ∃ a, (↑K f) a = c • f v
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
y : x ∈ (f + g).domain
hxy : x ∈ (g + f).domain
⊢ ↑(f + g) ⟨x, y⟩ = ↑(g + f) ⟨x, hxy⟩

Tactic:
· simp only [add_apply, add_comm]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case grade1
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x : X
⊢ ι R x ∈ S

Tactic:
| grade1 x =>

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

Goal state before:
pp: p : ℕ
⊢ Prime p ↔ 2 ≤ p ∧ ∀ (m n : ℕ), m < p → n < p → m * n ≠ p

Tactic:
prime_def_lt,

Goal state after:
p : ℕ
⊢ (2 ≤ p ∧ ∀ (m : ℕ), m < p → m ∣ p → m = 1) ↔ 2 ≤ p ∧ ∀ (m n : ℕ), m < p → n < p → m * n ≠ p
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type v
δ : Type x
inst✝ : Preorder β
f : α → β
s : Set α
a : α
t : Set δ
g : δ → α
b : δ
hf : IsMinOn f s a
hg : MapsTo g t s
ha : g b = a
y : δ
hy : y ∈ t
⊢ y ∈ {x | (fun x ↦ (f ∘ g) b ≤ (f ∘ g) x) x}

Tactic:
by
  simpa only [ha, (· ∘ ·)] using! hf (hg hy)

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

Goal state before:

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

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

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
g : M
r : R
c' : R[M]
_nm : g ∉ c'.coeff.support
_nz : ¬r = 0
w : f (c' • v) = c' • f v
⊢ f ((algebraMap R R[M]) r • (of R M) g • v) + c' • f v = (algebraMap R R[M]) r • (of R M) g • f v + c' • f v

Tactic:
algebraMap_smul,

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
g : M
r : R
c' : R[M]
_nm : g ∉ c'.coeff.support
_nz : ¬r = 0
w : f (c' • v) = c' • f v
⊢ f (r • (of R M) g • v) + c' • f v = (algebraMap R R[M]) r • (of R M) g • f v + c' • f v
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
g : M
r : R
c' : R[M]
_nm : g ∉ c'.coeff.support
_nz : ¬r = 0
w : f (c' • v) = c' • f v
⊢ f (r • (of R M) g • v) + c' • f v = (algebraMap R R[M]) r • (of R M) g • f v + c' • f v

Tactic:
algebraMap_smul,

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
g : M
r : R
c' : R[M]
_nm : g ∉ c'.coeff.support
_nz : ¬r = 0
w : f (c' • v) = c' • f v
⊢ f (r • (of R M) g • v) + c' • f v = r • (of R M) g • f v + c' • f v
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List R[A]
⊢ Quot.lift (fun l ↦ List.foldr (fun x1 x2 ↦ x1 ⊓ x2) ⊤ l) ⋯ (Multiset.map degt l.prod.coeff.support.val) ≤
    List.foldr (fun x1 x2 ↦ x1 + x2) 0 (List.map (fun f ↦ f.coeff.support.inf degt) l)

Tactic:
refine sup_support_list_prod_le ?_ ?_ l

Goal state after:
case refine_1
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List R[A]
⊢ degt 0 ≤ 0

case refine_2
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List R[A]
⊢ ∀ (a b : A), degt (a + b) ≤ degt a + degt b
Module: Mathlib.Algebra.Polynomial.Coeff

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

Tactic:
coeff_X_pow_mul Q n i

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
P Q : R[X]
hPQ : X ^ n * P = X ^ n * Q
i : ℕ
⊢ Q.coeff i = Q.coeff i
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : 0 < ↑p.natDegree
⊢ (p + C a).natDegree = p.natDegree

Tactic:
Nat.cast_pos,

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : 0 < p.natDegree
⊢ (p + C a).natDegree = p.natDegree
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case hb
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
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ supDegree D p + supDegree D q ∈ { toFun := D, map_add' := hadd }.srange

pp: case hb
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
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ ∀ {a b : B}, a ∈ Set.range D → b ∈ Set.range D → a + b ∈ Set.range D

Tactic:
· exact add_mem (supDegree_mem_range D hp) (supDegree_mem_range D hq)

Goal state after:
case hb
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
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ ∀ {a b : B}, a ∈ Set.range D → b ∈ Set.range D → a + b ∈ Set.range D
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
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✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq0 : q = 0
⊢ (p * q).degree = p.degree + q.degree

Tactic:
by simp only [hq0, degree_zero, mul_zero, WithBot.add_bot]

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:
simp [adjoin_singleton_eq_range_aeval]

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

Goal state before:
pp: S : Type v
A' : Type u_1
inst✝² : CommSemiring A'
inst✝¹ : CommSemiring S
inst✝ : Algebra S A'
x✝ : A'
⊢ (aevalTower (Algebra.ofId S A') x✝) X = (aeval x✝) X

Tactic:
simp only [aeval_X, aevalTower_X]

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

Goal state before:
pp: case monomial
R : Type u
A : Type z
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
q : Submodule R M
m : M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hm : m ∈ q
a : A
hq : q ≤ Submodule.comap ((Algebra.lsmul R R M) a) q
n : ℕ
t : R
hmq : (aeval a) (C t * X ^ n) • m ∈ q
⊢ (aeval a) (C t * X ^ (n + 1)) • m ∈ q

Tactic:
rw [pow_succ', mul_left_comm, map_mul, aeval_X, mul_smul]
    solve_by_elim

Goal state after:
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₂Hom f g) (eval₂ C q p)

Tactic:
rw [eval₂_comp_left (eval₂Hom f g)]

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₂ ((eval₂Hom f g).comp C) (⇑(eval₂Hom f g) ∘ q) p
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
⊢ (monomial i) x ∈ coeffsIn σ M ↔ x ∈ M

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

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : Disjoint p.degrees q.degrees
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ toMultiset d ≤ (p + q).degrees

Tactic:
Multiset.disjoint_iff_ne

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ toMultiset d ≤ (p + q).degrees
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
⊢ coeff d p - c = 0

Tactic:
hc,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
⊢ c - c = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
i : σ
a : R
ha : a ≠ 0
⊢ Multiset.count i (toMultiset s) = s i

Tactic:
Finsupp.count_toMultiset

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
i : σ
a : R
ha : a ≠ 0
⊢ s i = s i