mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
m : ↥N
⊢ ⇑(snf.bM.repr ↑m) ∘ ⇑snf.f = snf.a • ⇑(snf.bN.repr m)

Tactic:
by
  ext i
  simp [Pi.smul_apply (snf.a i)]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
m : A
⊢ mk ((algebraMap A R) m) 1 = (algebraMap A (Localization M)) m

Tactic:
rw [mk_eq_mk', mk'_eq_iff_eq_mul, Submonoid.coe_one, map_one, mul_one]

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
m : A
⊢ (algebraMap R (Localization M)) ((algebraMap A R) m) = (algebraMap A (Localization M)) m
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ Algebra.IsEpi R A ↔ ∀ (a : A), 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1

Tactic:
refine ⟨fun h a ↦ IsEpi.injective_lift_mul <| by simp, fun h ↦ ⟨fun x y hxy ↦ ?_⟩⟩
  have h' (x : A ⊗[R] A) : ∃ a : A, x = a ⊗ₜ 1 := by
    induction x using TensorProduct.induction_on with
    | zero => exact ⟨0, by simp⟩
    | tmul u v =>
      use u * v
      calc u ⊗ₜ[R] v = u ⊗ₜ[R] 1 * 1 ⊗ₜ[R] v := by simp
                   _ = u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1 := by rw [h]
                   _ = (u * v) ⊗ₜ[R] 1 := by simp
    | add u v hu hv =>
      obtain ⟨u, rfl⟩ := hu
      obtain ⟨v, rfl⟩ := hv
      exact ⟨u  + v, by simp [add_tmul]⟩
  obtain ⟨a, rfl⟩ := h' x
  obtain ⟨b, rfl⟩ := h' y
  aesop

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : ⊤ = R ∙ x
⊢ ∃ I f, I ≠ ⊤ ∧ Surjective ⇑f

Tactic:
let f := (LinearMap.toSpanSingleton R _ x).quotKerEquivOfSurjective
    (by rw [← LinearMap.range_eq_top, ← LinearMap.span_singleton_eq_range, hx])

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : ⊤ = R ∙ x
f : (R ⧸ (LinearMap.toSpanSingleton R (M ⧸ N) x).ker) ≃ₗ[R] M ⧸ N :=
  (LinearMap.toSpanSingleton R (M ⧸ N) x).quotKerEquivOfSurjective ⋯
⊢ ∃ I f, I ≠ ⊤ ∧ Surjective ⇑f
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsEpi R A
a✝ b✝ a b : A
⊢ a ⊗ₜ[R] b = a • 1 ⊗ₜ[R] b

Tactic:
by rw [tmul_eq_smul_one_tmul]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsEpi R A
a✝ b✝ a b : A
⊢ a • b ⊗ₜ[R] 1 = a • b • 1 ⊗ₜ[R] 1

Tactic:
by rw [tmul_eq_smul_one_tmul]

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✝³ : AddCommMonoidWithOne A
inst✝² : Module R A
inst✝¹ : AddCommMonoidWithOne B
inst✝ : Module R B
n : ℕ
⊢ ↑n = 1 ⊗ₜ[R] ↑n

Tactic:
by
  rw [natCast_def, ← nsmul_one, smul_tmul, nsmul_one]

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
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 - y * x) * (1 + y * h.unit.inv * x) = 1 - y * x + y * ((1 - x * y) * h.unit.inv) * x

Tactic:
by noncomm_ring

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
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 + y * h.unit.inv * x) * (1 - y * x) = 1 - y * x + y * (h.unit.inv * (1 - x * y)) * x

Tactic:
by noncomm_ring

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

Goal state before:
pp: F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : NonUnitalRing B
inst✝⁸ : Module R S
inst✝⁷ : Module S A
inst✝⁶ : Module R A
inst✝⁵ : Module S B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R S A
inst✝² : IsScalarTower R S B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F S A B
φ : F
a : A
⊢ quasispectrum R (φ a) ⊆ quasispectrum R a

Tactic:
refine Set.compl_subset_compl.mp fun x ↦ ?_

Goal state after:
F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : NonUnitalRing B
inst✝⁸ : Module R S
inst✝⁷ : Module S A
inst✝⁶ : Module R A
inst✝⁵ : Module S B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R S A
inst✝² : IsScalarTower R S B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F S A B
φ : F
a : A
x : R
⊢ x ∈ (quasispectrum R a)ᶜ → x ∈ (quasispectrum R (φ a))ᶜ
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: case refine_1
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Algebra R S
a : A
f : S → R
inst✝² : IsScalarTower S A A
inst✝¹ : SMulCommClass S A A
inst✝ : IsScalarTower R S A
h : QuasispectrumRestricts a f
⊢ ⇑(algebraMap R S) '' quasispectrum R a ⊆ quasispectrum S a

pp: case refine_2
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Algebra R S
a : A
f : S → R
inst✝² : IsScalarTower S A A
inst✝¹ : SMulCommClass S A A
inst✝ : IsScalarTower R S A
h : QuasispectrumRestricts a f
s : S
hs : s ∈ quasispectrum S a
⊢ f s ∈ quasispectrum R a ∧ (algebraMap R S) (f s) = s

Tactic:
· simpa only [quasispectrum.preimage_algebraMap] using
      (quasispectrum S a).image_preimage_subset (algebraMap R S)

Goal state after:
case refine_2
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Algebra R S
a : A
f : S → R
inst✝² : IsScalarTower S A A
inst✝¹ : SMulCommClass S A A
inst✝ : IsScalarTower R S A
h : QuasispectrumRestricts a f
s : S
hs : s ∈ quasispectrum S a
⊢ f s ∈ quasispectrum R a ∧ (algebraMap R S) (f s) = s
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : SMulCommClass R A A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
φ : A →⋆ₙₐ[R] B
hφ : Function.Surjective ⇑φ
⊢ Function.Surjective ⇑(starMap φ)

Tactic:
intro x
  induction x using Unitization.ind with
  | inl_add_inr r b =>
    obtain ⟨a, rfl⟩ := hφ b
    exact ⟨mk (r, a), by rfl⟩

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

Goal state before:
pp: A : Type u_1
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
u a : A
hu : IsUnit u
⊢ 0 ≤ a ∧ IsUnit (u * a * star u) ↔ 0 ≤ a ∧ IsUnit a

Tactic:
lift u to Aˣ using hu

Goal state after:
A : Type u_1
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
u : Aˣ
⊢ 0 ≤ a ∧ IsUnit (↑u * a * star ↑u) ↔ 0 ≤ a ∧ IsUnit a
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : a ≤ b
⊢ IsSelfAdjoint a ↔ IsSelfAdjoint b

Tactic:
by
  replace hab := (sub_nonneg.mpr hab).isSelfAdjoint
  aesop (add simp IsSelfAdjoint)

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : ↑(ofVectorSpaceIndex K V)
⊢ (ofVectorSpace K V) x = ↑x

Tactic:
unfold ofVectorSpace

Goal state after:
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : ↑(ofVectorSpaceIndex K V)
⊢ (extend ⋯) x = ↑x
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: case inr
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 : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : x ∈ adjoin R s), p x hx → p (r • x) ⋯
star : ∀ (x : A) (hx : x ∈ adjoin R s), p x hx → p (Star.star x) ⋯
a : A
ha : a ∈ adjoin R s
x : A
hx✝ : x ∈ s ∪ Star.star s
hx : Star.star x ∈ s
⊢ p x ⋯

Tactic:
simpa using star _ (NonUnitalAlgebra.subset_adjoin R (by simpa using Or.inl hx)) (mem _ hx)

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : StrongRankCondition R
v : M
n : v ≠ 0
h : ∀ (w : M), ∃ c, c • v = w
this : Nontrivial R
⊢ Module.rank R M = 1

Tactic:
obtain ⟨b⟩ := (Basis.basis_singleton_iff.{_, _, u} PUnit).mpr ⟨v, n, h⟩

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : StrongRankCondition R
v : M
n : v ≠ 0
h : ∀ (w : M), ∃ c, c • v = w
this : Nontrivial R
b : Basis PUnit.{u + 1} R M
⊢ Module.rank R M = 1
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
h : Module.Finite R M ∧ Finite ι
⊢ Module.Finite R (ι →₀ M)

Tactic:
by cases h; infer_instance

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 : Set A
hcomm✝ : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : adjoin R s ≤ centralizer R ↑(centralizer R s)
x✝¹ : A
h₁ : x✝¹ ∈ adjoin R s
x✝ : A
h₂ : x✝ ∈ adjoin R s
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
apply this at h₁

Goal state after:
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 : Set A
hcomm✝ : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : adjoin R s ≤ centralizer R ↑(centralizer R s)
x✝¹ x✝ : A
h₂ : x✝ ∈ adjoin R s
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : x✝¹ ∈ centralizer R ↑(centralizer R s)
⊢ x✝¹ * x✝ = x✝ * x✝¹
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
this : Nontrivial K
h : Module.rank K V = 1
v₀ : V
hzero : v₀ = 0
hv : ∀ (v : V), 0 = v
x✝¹ x✝ : V
⊢ x✝¹ = x✝

Tactic:
by simp_rw [← hv]

Goal state after:
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
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
⊢ IsUnit f ↔ f.range = ⊤

Tactic:
isUnit_iff_ker_eq_bot,

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
⊢ f.ker = ⊥ ↔ f.range = ⊤
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ mdvd : m ∣ p
k : ℕ
e✝ : p = m * k
e : p = k * m
h✝ : mdvd = ⋯
hk : k ≤ p.sqrt
⊢ 1 * m < k * m

Tactic:
rwa [one_mul, ← e]

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

Goal state before:
pp: n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
⊢ Prime n

Tactic:
by
  refine prime_def_lt.mpr ⟨h1, fun m mlt mdvd => ?_⟩
  have hm : m ≠ 0 := by
    rintro rfl
    rw [zero_dvd_iff] at mdvd
    exact mlt.ne' mdvd
  exact (h m mlt hm).symm.eq_one_of_dvd mdvd

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : a ∈ s
hfsa : IsMinOn f s a
⊢ ∀ (b : β), b ≤ f a ↔ b ∈ lowerBounds {x | ∃ x_1 ∈ s, f x_1 = x}

Tactic:
intro b

Goal state after:
α : Type u
β : Type v
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : a ∈ s
hfsa : IsMinOn f s a
b : β
⊢ b ≤ f a ↔ b ∈ lowerBounds {x | ∃ x_1 ∈ s, f x_1 = x}
Module: Mathlib.Algebra.Polynomial.Coeff

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

Tactic:
by
  rcases p with ⟨p⟩
  simp_rw [← monomial_zero_left, ← ofFinsupp_single, ← ofFinsupp_mul, coeff]
  exact p.coeff_mul_single_zero a n

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

Goal state before:
pp: 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

pp: 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

Tactic:
· refine (OrderDual.ofDual_le_ofDual.mp ?_)
    exact degt0

Goal state after:
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.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : 0 < n
⊢ p.degree = ↑n ↔ p.natDegree = n

Tactic:
obtain rfl | h := eq_or_ne p 0
  · simp [hn.ne]
  · exact degree_eq_iff_natDegree_eq h

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

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

Tactic:
simp [mul_sub]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
c : R
hc : (C c).Monic
⊢ c ≠ 0

Tactic:
rintro rfl
  simp [Monic] at hc

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

Goal state before:
pp: case h₁
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 q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ap ∉ p.coeff.support → (∑ x ∈ q.coeff.support, if ap + x = ap + aq then p.coeff ap * q.coeff x else 0) = 0

Tactic:
· refine fun h => Finset.sum_eq_zero (fun a _ => ite_eq_right_iff.mpr <| fun _ => ?_)
    rw [Finsupp.notMem_support_iff.mp h, zero_mul]

Goal state after:
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 ∈ p.support, b ≠ p.natDegree → (fun a b ↦ (C b * q ^ a).coeff (p.natDegree * q.natDegree)) b (p.coeff b) = 0

Tactic:
intro b

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
⊢ b ∈ p.support → 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
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ ∀ b ∈ range (p.natDegree + 1), b ≠ n → p.coeff b * (r ^ b * if n = b then 1 else 0) = 0

Tactic:
intro b

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n b : ℕ
⊢ b ∈ range (p.natDegree + 1) → b ≠ n → p.coeff b * (r ^ b * if n = b then 1 else 0) = 0
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: case inr
α : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : 0 ≤ fun x1 x2 ↦ g x1 x2
a : α
H : f a ≠ 0
⊢ ∑ a_1 ∈ (single a (f a)).support, g a_1 ((single a (f a)) a_1) ≤ f.sum g

Tactic:
support_single _ H,

Goal state after:
case inr
α : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : 0 ≤ fun x1 x2 ↦ g x1 x2
a : α
H : f a ≠ 0
⊢ ∑ a_1 ∈ {a}, g a_1 ((single a (f a)) a_1) ≤ f.sum g
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
β : Type u_4
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
f g : ι →₀ α
inst✝ : IsBotZeroClass α
⊢ ∀ (a : ι →₀ α), 0 ≤ a

Tactic:
simp [le_def]

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

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
φ : R[X] →ₐ[R] A
p : R[X]
⊢ φ p = eval₂ (algebraMap R A) (φ X) p

Tactic:
rw [← aeval_def, aeval_algHom, aeval_X_left, AlgHom.comp_id]

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 : ι), IsBotZeroClass (α i)
⊢ ∀ (a : Π₀ (i : ι), α i), 0 ≤ a

Tactic:
simp [le_def]

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✝ : DecidableEq ι
f : Π₀ (i : ι), α i
i : ι
a : α i
⊢ single i a ≤ f ↔ a ≤ f i

Tactic:
classical exact (le_iff' support_single_subset).trans <| by simp

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
m : σ →₀ ℕ
⊢ m ∈ p.support \ q.support → m ∈ (p + q).support

Tactic:
hm

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
m : σ →₀ ℕ
hm : m ∈ p.support \ q.support
⊢ m ∈ (p + q).support
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
⊢ IsLeftRegular ((MvPolynomial.monomial m) a)

Tactic:
intro p q h

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
p q : MvPolynomial σ R
h : (fun x ↦ (MvPolynomial.monomial m) a * x) p = (fun x ↦ (MvPolynomial.monomial m) a * x) q
⊢ p = q
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
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
hor : ∀ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 → coeff n p ≠ 0 ∨ coeff n q ≠ 0
n : σ →₀ ℕ
hn : ¬coeff n q = 0
⊢ ¬coeff n p + coeff n q = 0 ∧ coeff n q = coeff n p + coeff n q

Tactic:
simp [hr n hn, hn]

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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Injective ⇑f
⊢ Injective ⇑(map f)

Tactic:
intro p q h

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Injective ⇑f
p q : MvPolynomial σ R
h : (map f) p = (map f) q
⊢ p = q
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
s : Set S₁
⊢ Algebra.adjoin R s = (aeval Subtype.val).range

Tactic:
← Algebra.adjoin_range_eq_range_aeval,

Goal state after:
R : Type u
S₁ : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
s : Set S₁
⊢ Algebra.adjoin R s = Algebra.adjoin R (range Subtype.val)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f : R →+* S
p : MvPolynomial σ R
s : subS
hs : ∀ i ∈ p.support, f (coeff i p) ∈ s
v : σ → S
hv : ∀ (i : σ), v i ∈ s
⊢ eval₂ f v p ∈ s

Tactic:
classical
  replace hs : ∀ i, f (p.coeff i) ∈ s := by
    intro i
    by_cases hi : i ∈ p.support
    · exact hs i hi
    · rw [MvPolynomial.notMem_support_iff.1 hi, f.map_zero]
      exact zero_mem s
  induction p using MvPolynomial.monomial_add_induction_on with
  | C a =>
    simpa using hs 0
  | monomial_add a b f ha _ ih =>
    rw [eval₂_add, eval₂_monomial]
    refine add_mem (mul_mem ?_ <| prod_mem fun i _ => pow_mem (hv _) _) (ih fun i => ?_)
    · simpa [MvPolynomial.notMem_support_iff.1 ha] using hs a
    have := hs i
    rw [coeff_add, coeff_monomial] at this
    split_ifs at this with h
    · subst h
      rw [MvPolynomial.notMem_support_iff.1 ha, map_zero]
      exact zero_mem _
    · rwa [zero_add] at this

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f : R →+* S
p : MvPolynomial σ R
s : subS
hs : ∀ i ∈ p.support, f (coeff i p) ∈ s
v : σ → S
hv : ∀ (i : σ), v i ∈ s
⊢ eval₂ f v p ∈ s

Tactic:
by
  classical
  replace hs : ∀ i, f (p.coeff i) ∈ s := by
    intro i
    by_cases hi : i ∈ p.support
    · exact hs i hi
    · rw [MvPolynomial.notMem_support_iff.1 hi, f.map_zero]
      exact zero_mem s
  induction p using MvPolynomial.monomial_add_induction_on with
  | C a =>
    simpa using hs 0
  | monomial_add a b f ha _ ih =>
    rw [eval₂_add, eval₂_monomial]
    refine add_mem (mul_mem ?_ <| prod_mem fun i _ => pow_mem (hv _) _) (ih fun i => ?_)
    · simpa [MvPolynomial.notMem_support_iff.1 ha] using hs a
    have := hs i
    rw [coeff_add, coeff_monomial] at this
    split_ifs at this with h
    · subst h
      rw [MvPolynomial.notMem_support_iff.1 ha, map_zero]
      exact zero_mem _
    · rwa [zero_add] at this

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

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
j : τ
h : j ∈ ((rename f) φ).vars
⊢ ∃ i ∈ φ.vars, f i = j

Tactic:
by
  classical
  simpa only [exists_prop, Finset.mem_image] using vars_rename f φ h

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : (if n ≤ y then p.coeff (y - n) else 0) ≠ 0
⊢ n ≤ y

Tactic:
exact by_contra fun h => hy (if_neg h)

Goal state after: