mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Subring.closure (Set.range ⇑includeLeft ∪ Set.range ⇑includeRight) = ⊤

Tactic:
by
  rw [← top_le_iff]
  rintro x -
  induction x with
  | zero => exact zero_mem _
  | tmul x y =>
    convert_to (Algebra.TensorProduct.includeLeftRingHom (R := R) x) *
      (Algebra.TensorProduct.includeRight y) ∈ _
    · simp
    · exact mul_mem (Subring.subset_closure (.inl ⟨x, rfl⟩))
        (Subring.subset_closure (.inr ⟨_, rfl⟩))
  | add x y _ _ => exact add_mem ‹_› ‹_›

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set B
hs : adjoin R s = ⊤
⊢ Subalgebra.toSubmodule (adjoin A ↑(Subalgebra.map includeRight ⊤)) = ⊤

Tactic:
← top_le_iff,

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set B
hs : adjoin R s = ⊤
⊢ ⊤ ≤ Subalgebra.toSubmodule (adjoin A ↑(Subalgebra.map includeRight ⊤))
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ ((mk R S M) 1).range = ⊤

Tactic:
← top_le_iff,

Goal state after:
R : Type u_1
M : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ ⊤ ≤ ((mk R S M) 1).range
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
S : Type u_3
T : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
⊢ ((mk R S T).flip 1).range = ⊤

Tactic:
← top_le_iff,

Goal state after:
R : Type u_1
S : Type u_3
T : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
⊢ ⊤ ≤ ((mk R S T).flip 1).range
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
hx : IsUnit (1 + x)
⊢ IsQuasiregular x

Tactic:
rw [isQuasiregular_iff]

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
hx : IsUnit (1 + x)
⊢ ∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0
Module: Mathlib.Algebra.Algebra.Spectrum.Pi

Goal state before:
pp: ι : Type u_1
κ : ι → Type u_5
inst✝ : (i : ι) → NonUnitalSemiring (κ i)
x : (i : ι) → κ i
⊢ IsQuasiregular x ↔ ∀ (i : ι), IsQuasiregular (x i)

Tactic:
by
  simp only [isQuasiregular_iff', ← isUnit_map_iff (PreQuasiregular.toPi κ), Pi.isUnit_iff]
  congr!

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

Goal state before:
pp: case inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
s : S
r✝ : R
a✝ : A
⊢ s • inl r✝ + s • ↑a✝ = s • inl r✝ + (s • 1) • ↑a✝

Tactic:
smul_one_smul

Goal state after:
case inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
s : S
r✝ : R
a✝ : A
⊢ s • inl r✝ + s • ↑a✝ = s • inl r✝ + s • ↑a✝
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y✝ x y : R
hle : ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y = x + p
z s : R
hs : s ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y = x + s
⊢ s ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y + z = x + z + s

Tactic:
rw [hs.2, add_right_comm]

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y✝ x y : R
hle : ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y = x + p
z s : R
hs : s ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y = x + s
⊢ s ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ x + z + s = x + z + s
Module: Mathlib.Algebra.Algebra.Subalgebra.Directed

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra 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)
T : Subalgebra R A
hT : T ≤ iSup K
i : ι
⊢ ∀ (j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩

Tactic:
j

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra 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)
T : Subalgebra R A
hT : T ≤ iSup K
i j : ι
⊢ ∀ (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : NonUnitalSemiring A
inst✝³ : StarRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
⊢ ↑(centralizer R ↑(centralizer R s)) = (s ∪ star s).centralizer.centralizer

Tactic:
by
  rw [coe_centralizer, StarMemClass.star_coe_eq, Set.union_self, coe_centralizer]

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✝² : Finite K
inst✝¹ : Free K V
inst✝ : Module.Finite K V
⊢ lift.{u, v} #V < ℵ₀

Tactic:
lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank K V

Goal state after:
K : Type u
V : Type v
inst✝⁶ : Ring K
inst✝⁵ : StrongRankCondition K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Finite K
inst✝¹ : Free K V
inst✝ : Module.Finite K V
⊢ lift.{v, u} #K ^ lift.{u, v} (Module.rank K V) < ℵ₀
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case insert.h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
⊢ Commute (f i) (s.noncommProd f ⋯)

pp: case insert.h'
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
⊢ Disjoint (f i).ker (s.noncommProd f ⋯).ker

Tactic:
· exact s.noncommProd_commute _ _ _ fun j hj ↦
        comm (s.mem_insert_self i) (Finset.mem_insert_of_mem hj) (by lia)

Goal state after:
case insert.h'
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
⊢ Disjoint (f i).ker (s.noncommProd f ⋯).ker
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case refine_1
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
this : K ∙ v ≠ ⊥
⊢ K ∙ v ≤ S

Tactic:
span_le,

Goal state after:
case refine_1
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
this : K ∙ v ≠ ⊥
⊢ {v} ⊆ ↑S
Module: Mathlib.Algebra.FreeAlgebra

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

Tactic:
change (_ + _) * _ = _ * _ + _ * _
        rw [right_distrib]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p r : R[X]
k : ℕ
⊢ (p * X ^ k).comp r = p.comp r * r ^ k

Tactic:
by
  induction k with
  | zero => simp
  | succ k ih => simp [ih, pow_succ, ← mul_assoc, mul_X_comp]

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

Goal state before:
pp: R : Type u
a : R
inst✝ : CommSemiring R
p q : R[X]
H : p.IsRoot a
⊢ (p * q).IsRoot a

Tactic:
by rw [IsRoot, eval_mul, IsRoot.def.1 H, zero_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mp
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
M : Type u_7
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : Module R F
inst✝ : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
y : ↥(z • f).domain
hy : ↑y = (x_fst, x_snd).1
h : z • ↑f y = (x_fst, x_snd).2
⊢ ∃ a a_1, ↑a_1 = a ∧ a = x_fst ∧ z • ↑f a_1 = x_snd

Tactic:
use x_fst, y, hy

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

Goal state before:
pp: n : ℕ
⊢ 0 < n.minFac

Tactic:
by_cases n1 : n = 1
  · simp [n1]
  · exact (minFac_prime n1).pos

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mp
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
x_fst : E
x_snd : F
y : ↥(-f).domain
hy : ↑y = (x_fst, x_snd).1
h : -↑f y = (x_fst, x_snd).2
⊢ ∃ a a_1, ↑a_1 = a ∧ a = x_fst ∧ -↑f a_1 = x_snd

Tactic:
use x_fst, y, hy

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

Goal state before:
pp: n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
⊢ n.minFac ≤ n.minFac * (x + 2) / n.minFac

Tactic:
Nat.mul_div_cancel_left _ (minFac_pos _)

Goal state after:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
⊢ n.minFac ≤ x + 2
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type v
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
D : α → β
s : Finset α
inst✝ : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_1 ∈ s, D a_1 ≤ D a
a✝ : α
⊢ a✝ ∈ ↑s → a✝ ∈ {x | (fun x ↦ D x ≤ D (Function.invFun D (D a))) x}

Tactic:
Function.apply_invFun_apply (f := D)

Goal state after:
α : Type u
β : Type v
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
D : α → β
s : Finset α
inst✝ : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_1 ∈ s, D a_1 ≤ D a
a✝ : α
⊢ a✝ ∈ ↑s → a✝ ∈ {x | (fun x ↦ D x ≤ D a) x}
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_1
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ supDegree D (∏ i ∈ ∅, f i) ≤ ∑ i ∈ ∅, supDegree D (f i)

Tactic:
rw [Finset.prod_empty, Finset.sum_empty, one_def, supDegree_single]

Goal state after:
case refine_1
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ (if 1 = 0 then ⊥ else D 0) ≤ 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : 0 < p.natDegree
⊢ p.nextCoeff = p.coeff (p.natDegree - 1)

Tactic:
rw [nextCoeff, if_neg]
  contrapose! hp
  simpa

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p ^ n).degree + p.degree ≤ n • p.degree + p.degree

Tactic:
degree_pow_le

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ n • p.degree + p.degree ≤ n • p.degree + p.degree
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : (monomial p.natDegree) p.leadingCoeff + erase p.natDegree p = p
hq : (monomial q.natDegree) q.leadingCoeff + erase q.natDegree q = q
hd' : p.natDegree = q.natDegree
hq0 : q ≠ 0
| (p - q).degree

Tactic:
← hp,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : (monomial p.natDegree) p.leadingCoeff + erase p.natDegree p = p
hq : (monomial q.natDegree) q.leadingCoeff + erase q.natDegree q = q
hd' : p.natDegree = q.natDegree
hq0 : q ≠ 0
| ((monomial p.natDegree) p.leadingCoeff + erase p.natDegree p - q).degree
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : (monomial p.natDegree) p.leadingCoeff + erase p.natDegree p = p
hq : (monomial q.natDegree) q.leadingCoeff + erase q.natDegree q = q
hd' : p.natDegree = q.natDegree
hq0 : q ≠ 0
| ((monomial q.natDegree) q.leadingCoeff + erase q.natDegree p -
      ((monomial q.natDegree) q.leadingCoeff + erase q.natDegree q)).degree

Tactic:
add_sub_add_left_eq_sub,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : (monomial p.natDegree) p.leadingCoeff + erase p.natDegree p = p
hq : (monomial q.natDegree) q.leadingCoeff + erase q.natDegree q = q
hd' : p.natDegree = q.natDegree
hq0 : q ≠ 0
| (erase q.natDegree p - erase q.natDegree q).degree
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h₁ : p ∣ q
h₂ : q.natDegree < p.natDegree
hc : ¬q = 0
⊢ False

Tactic:
exact lt_iff_not_ge.mp h₂ (natDegree_le_of_dvd h₁ hc)

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
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 * q) = supDegree D p + supDegree D q

Tactic:
apply supDegree_eq_of_max

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
⊢ supDegree D p + supDegree D q ∈ Set.range D

case hmem
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
⊢ Function.invFun D (supDegree D p + supDegree D q) ∈ (p * q).coeff.support

case hmax
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 ∈ (p * q).coeff.support, D a ≤ supDegree D p + supDegree D q
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree < q.degree
⊢ (p - q).degree = q.degree

Tactic:
rw [← degree_neg q] at h
  rw [sub_eq_add_neg, degree_add_eq_right_of_degree_lt h, degree_neg]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝⁷ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : LinearOrder B
inst✝³ : OrderBot B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst✝ : Nontrivial R
hp : Monic D p
⊢ supDegree D 1 = 0 • supDegree D p

Tactic:
zero_nsmul,

Goal state after:
case zero
R : Type u_1
inst✝⁷ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : LinearOrder B
inst✝³ : OrderBot B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst✝ : Nontrivial R
hp : Monic D p
⊢ supDegree D 1 = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : SemilatticeInf T
inst✝ : OrderTop T
D : A → T
s : R[A]
hs : s.coeff.support.Nonempty
⊢ infDegree (WithTop.some ∘ D) s = ↑(infDegree D s)

Tactic:
by
  unfold AddMonoidAlgebra.infDegree
  rw [← Finset.coe_inf' hs, Finset.inf'_eq_inf]

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:
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.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f1 f2 : ι →₀ α
⊢ (f1 - f2).support ⊆ f1.support

Tactic:
simp +contextual only [subset_iff, tsub_eq_zero_iff_le, mem_support_iff,
    Ne, coe_tsub, Pi.sub_apply, not_imp_not, zero_le, imp_true_iff]

Goal state after:
Module: Mathlib.Data.DFinsupp.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (α i)
inst✝⁵ : (i : ι) → PartialOrder (α i)
inst✝⁴ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝³ : (i : ι) → Sub (α i)
inst✝² : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ (f - g).support ⊆ f.support

Tactic:
simp +contextual only [subset_iff, tsub_eq_zero_iff_le, mem_support_iff,
    Ne, coe_tsub, Pi.sub_apply, not_imp_not, zero_le, imp_true_iff]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i : ℕ
⊢ ∀ (b : ℕ), i + b = l + m → (i = l → ¬b = m) → P.coeff i * Q.coeff b = 0

Tactic:
j

Goal state after:
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
⊢ i + j = l + m → (i = l → ¬j = m) → P.coeff i * Q.coeff j = 0
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (a : R) {p : MvPolynomial σ R}, eval₂ f g (p * C a) = eval₂ f g p * eval₂ f g (C a)

Tactic:
simp [eval₂_C, eval₂_mul_C]

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
hle : ⇑x ≤ ⇑y
j : ι
hlt : x j < y j
this : (↑(x.neLocus y)).WellFoundedOn r
i : { x_1 // x_1 ∈ ↑(x.neLocus y) }
hi : i ∈ {i | x ↑i < y ↑i}
hl : ∀ x_1 ∈ {i | x ↑i < y ↑i}, ¬Subrel r (fun x_2 ↦ x_2 ∈ ↑(x.neLocus y)) x_1 i
⊢ ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

Tactic:
refine ⟨i, fun k hk ↦ ⟨hle k, ?_⟩, hi⟩

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
this : (↑(x.neLocus y)).WellFoundedOn r
i : { x_1 // x_1 ∈ ↑(x.neLocus y) }
hi : i ∈ {i | x ↑i < y ↑i}
hl : ∀ x_1 ∈ {i | x ↑i < y ↑i}, ¬Subrel r (fun x_2 ↦ x_2 ∈ ↑(x.neLocus y)) x_1 i
k : ι
hk : r k ↑i
⊢ y k ≤ x k
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ ((p + q).support.sup fun s ↦ toMultiset s) ≤ (p.support.sup fun s ↦ toMultiset s) ⊔ q.support.sup fun s ↦ toMultiset s

Tactic:
exact supDegree_add_le

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

Goal state before:
pp: case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ a ∈ p.degrees, ∃ b ∈ q.degrees, a = b

Tactic:
refine ⟨j, ?_, j, ?_, rfl⟩

Goal state after:
case inr.refine_1
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ j ∈ p.degrees

case inr.refine_2
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ j ∈ q.degrees
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f g : MvPolynomial σ R
⊢ ((f + g).support.sup fun m ↦ m n) ≤ max (f.support.sup fun m ↦ m n) (g.support.sup fun m ↦ m n)

Tactic:
exact supDegree_add_le

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i j : σ
k : ℕ
h : i ≠ j
⊢ degreeOf i (p * X j ^ k) = degreeOf i p

Tactic:
by
  induction k with
  | zero => rw [pow_zero, mul_one]
  | succ k hk => rw [pow_add, pow_one, ← mul_assoc, degreeOf_mul_X_of_ne _ h, hk]

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

Goal state before:
pp: R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
n m : σ✝
s : σ✝ →₀ ℕ
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ algebraMap R (MvPolynomial σ S) =
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).comp (algebraMap R (MvPolynomial σ R))

Tactic:
by ext; simp [C, monomial, map]

Goal state after: