mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝⁴ : Fintype m
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Finite l
inst✝ : DecidableEq m
A : Matrix l m R
B : Matrix m n R
⊢ (toLin v₁ v₃) (A * B) = (toLin v₂ v₃) A ∘ₗ (toLin v₁ v₂) B

Tactic:
by
  apply (LinearMap.toMatrix v₁ v₃).injective
  have : DecidableEq l := fun _ _ ↦ Classical.propDecidable _
  rw [LinearMap.toMatrix_comp v₁ v₂ v₃]
  repeat' rw [LinearMap.toMatrix_toLin]

Goal state after:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
A : Type u_4
inst✝ : CommRing A
K : Type u_5
x : ℤ
⊢ ∃ c, ↑c * x = ↑c * x

Tactic:
use 1

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

Goal state before:
pp: α : Type u_1
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
s t : Set α
⊢ (s + t)⋆ = s⋆ + t⋆

Tactic:
by
  simp_rw [← image_star, ← image2_add, image_image2, image2_image_left, image2_image_right,
    star_add]

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

Goal state before:
pp: α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : Star α
inst✝ : TrivialStar α
s : Set α
x✝ : α
⊢ x✝ ∈ star ⁻¹' s ↔ x✝ ∈ s

Tactic:
simp [star_trivial]

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

Goal state before:
pp: case a.add
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
x✝ y✝ : A ⊗[R] M
a✝¹ : (liftBaseChange A l) x✝ ∈ Submodule.span A ↑l.range
a✝ : (liftBaseChange A l) y✝ ∈ Submodule.span A ↑l.range
⊢ (liftBaseChange A l) x✝ + (liftBaseChange A l) y✝ ∈ Submodule.span A ↑l.range

Tactic:
exact add_mem ‹_› ‹_›

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
⊢ r • (↑a⁻¹ * ↑a) - 1 * ↑a = r • 1 - ↑a

Tactic:
a.inv_mul,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
⊢ r • 1 - 1 * ↑a = r • 1 - ↑a
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case add
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
x y : A ⊗[R] B
a✝¹ : x ∈ Subring.closure (Set.range ⇑includeLeft ∪ Set.range ⇑includeRight)
a✝ : y ∈ Subring.closure (Set.range ⇑includeLeft ∪ Set.range ⇑includeRight)
⊢ x + y ∈ Subring.closure (Set.range ⇑includeLeft ∪ Set.range ⇑includeRight)

Tactic:
exact add_mem ‹_› ‹_›

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

Goal state before:
pp: R : Type u_1
Q : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
I : Submodule R R
q : Q
h : q ∈ I • ⊤
⊢ ∀ (x y : Q),
    x ∈ (↑(TensorProduct.lid R Q) ∘ₗ rTensor Q I.subtype).range →
      y ∈ (↑(TensorProduct.lid R Q) ∘ₗ rTensor Q I.subtype).range →
        x + y ∈ (↑(TensorProduct.lid R Q) ∘ₗ rTensor Q I.subtype).range

Tactic:
by simp +contextual [add_mem]

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

Goal state before:
pp: R : Type u_1
Q : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
I : Submodule R R
t : ↥I ⊗[R] Q
⊢ ∀ (x y : ↥I ⊗[R] Q),
    (↑(TensorProduct.lid R Q) ∘ₗ rTensor Q I.subtype) x ∈ I • ⊤ →
      (↑(TensorProduct.lid R Q) ∘ₗ rTensor Q I.subtype) y ∈ I • ⊤ →
        (↑(TensorProduct.lid R Q) ∘ₗ rTensor Q I.subtype) (x + y) ∈ I • ⊤

Tactic:
by simp +contextual [add_mem]

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

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
r : R
hr : ¬IsUnit r
h : r ∈ resolventSet R ↑a
⊢ IsUnit r

Tactic:
simpa [map_sub] using h.map (fstHom R A)

Goal state after:
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
r : R
hr : r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a b : A
hab : ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), b = a + p
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), r • b = r • a + p

Tactic:
obtain ⟨a, ha, rfl⟩ := hab

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
r : R
hr : r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a✝ a : A
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), r • (a✝ + a) = r • a✝ + p
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
φ : F
a : A
⊢ star (↑(NonUnitalAlgHomClass.toNonUnitalAlgHom φ) a) ∈
    (NonUnitalAlgHom.range (NonUnitalAlgHomClass.toNonUnitalAlgHom φ)).carrier

Tactic:
exact ⟨star a, map_star φ a⟩

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S T : NonUnitalStarSubalgebra R A
⊢ ∀ {x : A}, x ∈ S → x ∈ S ⊔ T

Tactic:
by
  rw [← SetLike.le_def]
  exact le_sup_left

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)
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ (x * y) =
      Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ x *
        Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ y

Tactic:
dsimp only [SetLike.coe_sort_coe, NonUnitalAlgHom.coe_comp, Function.comp_apply,
          inclusion_mk, Eq.ndrec, id_eq, eq_mpr_eq_cast, ZeroMemClass.coe_zero,
          AddSubmonoid.mk_add_mk, Set.inclusion_mk]
        apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· * ·))
        all_goals simp

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_1
⊢ Module.Finite R (ι →₀ M) → IsEmpty ι ∨ Subsingleton M ∨ Module.Finite R M ∧ Finite ι

Tactic:
simp only [or_iff_not_imp_left, not_subsingleton_iff_nontrivial, not_isEmpty_iff]
    rintro h ⟨i⟩ _
    obtain ⟨s, hs⟩ := id h
    exact ⟨.of_surjective (Finsupp.lapply (R := R) (M := M) i) (Finsupp.apply_surjective i),
       finite_of_span_finite_eq_top_finsupp s.finite_toSet hs⟩

Goal state after:
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
⊢ ↑(centralizer R Set.univ) = ↑(center R A)

Tactic:
coe_centralizer,

Goal state after:
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
⊢ (Set.univ ∪ star Set.univ).centralizer = ↑(center R A)
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:
coe_centralizer,

Goal state after:
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 s) ∪ star ↑(centralizer R s)).centralizer = (s ∪ star s).centralizer.centralizer
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
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
h' : Disjoint p f.ker
x : V
hx : x ∈ comap f p
y : V
hy : y ∈ p
hxy : (f.restrict h) ⟨y, hy⟩ = ⟨f x, hx⟩
⊢ f y = f x

Tactic:
simpa [Subtype.ext_iff] using hxy

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

Goal state before:
pp: case mpr
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
ι : Type u_1
inst✝ : Unique ι
⊢ Nonempty (Basis ι K V) → finrank K V = 1

Tactic:
rintro ⟨b⟩
    simpa using finrank_eq_card_basis b

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:
← rank_eq_one_iff

Goal state after:
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 ↔ Module.rank K V = 1
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : Disjoint f.domain g.domain
x : ↥f.domain
y : ↥g.domain
hxy : ↑x = ↑y
⊢ ↑f x = ↑g y

Tactic:
disjoint_def

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ x ∈ f.domain, x ∈ g.domain → x = 0
x : ↥f.domain
y : ↥g.domain
hxy : ↑x = ↑y
⊢ ↑f x = ↑g y
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mk
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
fst✝ : E
snd✝ : F
⊢ (fst✝, snd✝) ∈ f.graph ↔ ∃ y, ↑y = fst✝ ∧ ↑f y = snd✝

Tactic:
mem_graph_iff',

Goal state after:
case mk
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
fst✝ : E
snd✝ : F
⊢ (∃ y, (↑y, ↑f y) = (fst✝, snd✝)) ↔ ∃ y, ↑y = fst✝ ∧ ↑f y = snd✝
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
n1 : n ≠ 1
⊢ n.minFacProp n.minFac

Tactic:
by_cases n0 : n = 0
  · simp [n0, minFacProp]
  have n2 : 2 ≤ n := by
    revert n0 n1
    rcases n with (_ | _ | _) <;> simp [succ_le_succ]
  simp only [minFac_eq]
  by_cases d2 : 2 ∣ n <;> simp only [d2, ↓reduceIte]
  · exact ⟨le_rfl, d2, fun k k2 _ => k2⟩
  · refine
      minFacAux_has_prop n2 3 0 rfl fun m m2 d => (Nat.eq_or_lt_of_le m2).resolve_left (mt ?_ d2)
    exact fun e => e.symm ▸ d

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
p : ℕ
hR : ExpChar R p
⊢ p ≠ 0

Tactic:
by
  cases hR
  · exact one_ne_zero
  · exact ‹p.Prime›.ne_zero

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
⊢ ∃ q, ExpChar R q

Tactic:
obtain _ | ⟨p, ⟨hp⟩, _⟩ := CharP.exists' R

Goal state after:
case inl
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
h✝ : CharZero R
⊢ ∃ q, ExpChar R q

case inr
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
p : ℕ
right✝ : CharP R p
hp : Nat.Prime p
⊢ ∃ q, ExpChar R q
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
p : R[A]
a : A
hlt : p.coeff a ≠ 0
⊢ D a ≤ supDegree D p

Tactic:
exact Finset.le_sup (Finsupp.mem_support_iff.2 hlt)

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

Goal state before:
pp: 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 ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i)

Tactic:
refine s.induction ?_ ?_

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]
⊢ supDegree D (∏ i ∈ ∅, f i) ≤ ∑ i ∈ ∅, supDegree D (f i)

case refine_2
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]
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      supDegree D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i) →
        supDegree D (∏ i ∈ insert a s, f i) ≤ ∑ i ∈ insert a s, supDegree D (f i)
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).coeff (-p).natDegree = -p.coeff p.natDegree

Tactic:
natDegree_neg,

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).coeff p.natDegree = -p.coeff p.natDegree
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case mpr
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun i ↦ if i ∈ φ.support then c i else 0
⊢ C r ∣ φ

Tactic:
let ψ : R[X] := ∑ i ∈ φ.support, monomial i (c' i)

Goal state after:
case mpr
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun i ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i) (c' i)
⊢ C r ∣ φ
Module: Mathlib.Algebra.Polynomial.Degree.Support

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
H : p ≠ 0
⊢ p.natDegree ∈ p.support

Tactic:
rw [mem_support_iff]
  exact (not_congr leadingCoeff_eq_zero).mpr H

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
⊢ (0 ^ n).natDegree = n * natDegree 0

Tactic:
zero_pow hn0

Goal state after:
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
⊢ natDegree 0 = n * natDegree 0
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
hdeg : ↑n ≤ p.degree
⊢ ↑n ≤ ↑p.natDegree

Tactic:
degree_eq_natDegree <| ne_zero_of_coe_le_degree hdeg

Goal state after:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
hdeg : ↑n ≤ ↑p.natDegree
⊢ ↑n ≤ ↑p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
a : R
inst✝ : Ring R
p : R[X]
hp : 0 < p.degree
⊢ (p + -C a).degree = p.degree

Tactic:
← C_neg,

Goal state after:
R : Type u
a : R
inst✝ : Ring R
p : R[X]
hp : 0 < p.degree
⊢ (p + C (-a)).degree = p.degree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
⊢ (p + -C a).natDegree = p.natDegree

Tactic:
← C_neg,

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
⊢ (p + C (-a)).natDegree = p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

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

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

Goal state before:
pp: case inl
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
hp : Monic D p
hq : q ≠ 0
h✝ : Subsingleton R
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

pp: case inr
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
hp : Monic D p
hq : q ≠ 0
h✝ : Nontrivial R
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
· exact (hq (Subsingleton.elim _ _)).elim

Goal state after:
case inr
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
hp : Monic D p
hq : q ≠ 0
h✝ : Nontrivial R
⊢ supDegree D (p * q) = supDegree D p + supDegree D q
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
hn : 0 < n
r : R
⊢ (X ^ n + C r).leadingCoeff = 1

Tactic:
by
  nontriviality R
  rw [leadingCoeff, natDegree_X_pow_add_C, coeff_add, coeff_X_pow_self, coeff_C,
    if_neg (pos_iff_ne_zero.mp hn), add_zero]

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
R : Type u_3
inst✝¹ : CommRing R
a b : R
inst✝ : Invertible a
⊢ (C a * X + C b).comp (C ⅟a * (X - C b)) = X

Tactic:
simp [← C_mul, ← mul_assoc]

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
R : Type u_3
inst✝¹ : CommRing R
a b : R
inst✝ : Invertible a
⊢ (C ⅟a * (X - C b)).comp (C a * X + C b) = X

Tactic:
simp [← C_mul, ← mul_assoc]

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
t : R
⊢ (algEquivAevalXAddC t).symm = algEquivAevalXAddC (-t)

Tactic:
by
  simp [algEquivAevalXAddC, sub_eq_add_neg]

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✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
⊢ ∀ (a₁ a₂ : Lex ((i : ι) → β i)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
by
    rintro _ a₂ ⟨i, h, hi⟩
    obtain ⟨a, ha₁, ha₂⟩ := exists_between hi
    classical
      refine ⟨Function.update a₂ _ a, ⟨i, fun j hj => ?_, ?_⟩, i, fun j hj => ?_, ?_⟩
      · rw [h j hj]
        dsimp only at hj
        rw [Function.update_of_ne hj.ne a]
      · rwa [Function.update_self i a]
      · rw [Function.update_of_ne hj.ne a]
      · rwa [Function.update_self i a]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
⊢ (∃ n, ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q) ↔
    (∃ n, ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ n, ¬coeff n q = 0 ∧ r = coeff n q

Tactic:
have hl (n : σ →₀ ℕ) (hne : p.coeff n ≠ 0) : q.coeff n = 0 :=
    notMem_support_iff.mp <| h.notMem_of_mem_left_finset (mem_support_iff.mpr hne)

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
⊢ (∃ n, ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q) ↔
    (∃ n, ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ n, ¬coeff n q = 0 ∧ r = coeff n q
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝¹ : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
inst✝ : Decidable (↑s.support ⊆ range f)
⊢ (killCompl hf) ((monomial s) c) = if ↑s.support ⊆ range f then (monomial (Finsupp.comapDomain f s ⋯)) c else 0

Tactic:
by
  split_ifs with h
  · exact killCompl_monomial_eq_monomial_comapDomain_of_subset hf c h
  · exact killCompl_monomial_eq_zero_of_not_subset hf c h

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

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✝ : σ✝ →₀ ℕ
inst✝⁴ : CommSemiring R✝
inst✝³ : CommSemiring S₁
p✝ q : MvPolynomial σ✝ R✝
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M N : Submodule R S
p : MvPolynomial σ S
s : σ
i : σ →₀ ℕ
x : S
n : ℕ
⊢ ∀ {a b : MvPolynomial σ S},
    a ∈ {p | ∀ (i : σ →₀ ℕ), coeff i p ∈ M} →
      b ∈ {p | ∀ (i : σ →₀ ℕ), coeff i p ∈ M} → a + b ∈ {p | ∀ (i : σ →₀ ℕ), coeff i p ∈ M}

Tactic:
by simp +contextual [add_mem]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : ∃ a ∈ φ.coeff.support, (mapDomain.addMonoidHom f) a = d
⊢ False

Tactic:
obtain ⟨u, hu, rfl⟩ := H

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
hu : u ∈ φ.coeff.support
h : ∀ (u_1 : σ →₀ ℕ), Finsupp.mapDomain f u_1 = (mapDomain.addMonoidHom f) u → coeff u_1 φ = 0
⊢ False