mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: case hsp
R✝ : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst✝⁸ : Semiring R✝
inst✝⁷ : CommSemiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R✝ M
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun i ↦ ↑(bW i)) (surjInv ⋯ ∘ ⇑bQ)
br : ⇑W.mkQ ∘ b ∘ Sum.inr = ⇑bQ
⊢ ⊤ ≤ span R (range fun i ↦ ↑(bW i)) ⊔ span R (range (surjInv ⋯ ∘ ⇑bQ))

Tactic:
show Set.range (fun i ↦ (bW i : V)) = W.subtype '' (Set.range (fun i ↦ bW i)) by aesop,

Goal state after:
case hsp
R✝ : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst✝⁸ : Semiring R✝
inst✝⁷ : CommSemiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R✝ M
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun i ↦ ↑(bW i)) (surjInv ⋯ ∘ ⇑bQ)
br : ⇑W.mkQ ∘ b ∘ Sum.inr = ⇑bQ
⊢ ⊤ ≤ span R (⇑W.subtype '' range fun i ↦ bW i) ⊔ span R (range (surjInv ⋯ ∘ ⇑bQ))
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : ↥t → R
sum : ∑ i, g i • ↑i = 0
z : ↥t
nonzero : g z ≠ 0
⊢ ∑ e ∈ t, extend Subtype.val g 0 e • e = 0

Tactic:
← Finset.sum_finset_coe

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : ↥t → R
sum : ∑ i, g i • ↑i = 0
z : ↥t
nonzero : g z ≠ 0
⊢ ∑ i, extend Subtype.val g 0 ↑i • ↑i = 0
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : AddCommGroup V'
inst✝³ : Module K V
inst✝² : Module K V'
v✝ : ι → V
s t : Set V
x y z : V
inst✝¹ : Nontrivial V
inst✝ : Nontrivial V'
v : V
hv : v ≠ 0
w : V'
hw : w ≠ 0
this : v ∉ ⊥
g : V →ₗ[K] V'
left✝ : g ∘ₗ ⊥.subtype = 0
hg : g v = w
⊢ g v ≠ 0 v

Tactic:
simp_all

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

Goal state before:
pp: case h
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := ⋯
w : V
hw : ¬f w = 0 w
⊢ f ((f w)⁻¹ • w) = 1

Tactic:
simp_all

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

Tactic:
apply Set.iUnionLift_unary (coe_iSup_of_directed dir) _ (fun _ x => star x)
          (fun _ _ => rfl)

Goal state after:
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)
⊢ ∀ (i : ι) (x : ↑↑(K i)), (f i) (star x) = star ((f i) 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
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : FiniteDimensional K V
⊢ finrank K ↥(K ∙ x) = 1

Tactic:
exact finrank_span_singleton hx

Goal state after:
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 : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
⊢ f ≤ f.sup g h

Tactic:
refine ⟨le_sup_left, fun z₁ z₂ hz => ?_⟩
  rw [← add_zero (f _), ← g.map_zero]
  refine (sup_apply h _ _ _ ?_).symm
  simpa

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

Goal state before:
pp: p : ℕ
hp✝ : 2 ≤ p
m : ℕ
h : m < p
n : ℕ
hp : p = m * n
⊢ m = 1 → p ≤ n

Tactic:
simp_all

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

Goal state before:
pp: n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
h' : n.minFac < 2
this : n.minFac = 1
⊢ False

Tactic:
simp_all

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph = g.graph
⊢ f = g

Tactic:
apply dExt

Goal state after:
case h
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 g : E →ₗ.[R] F
h : f.graph = g.graph
⊢ f.domain = g.domain

case h'
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 g : E →ₗ.[R] F
h : f.graph = g.graph
⊢ ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: case add
R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Monoid M
φ₁ φ₂ : A[M] →ₐ[R] B
single_one_right : ∀ (m : M), φ₁ (single m 1) = φ₂ (single m 1)
single_one_left : φ₁.comp singleOneAlgHom = φ₂.comp singleOneAlgHom
x✝ y✝ : A[M]
a✝¹ : φ₁ x✝ = φ₂ x✝
a✝ : φ₁ y✝ = φ₂ y✝
⊢ φ₁ (x✝ + y✝) = φ₂ (x✝ + y✝)

Tactic:
simp_all

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

Goal state before:
pp: case add
R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Monoid M
φ₁ φ₂ : A[M] →ₐ[R] B
single_one_right : ∀ (m : M), φ₁ (single m 1) = φ₂ (single m 1)
single_one_left : φ₁.comp singleOneAlgHom = φ₂.comp singleOneAlgHom
x✝ y✝ : A[M]
a✝¹ : φ₁ x✝ = φ₂ x✝
a✝ : φ₁ y✝ = φ₂ y✝
⊢ φ₁ (x✝ + y✝) = φ₂ (x✝ + y✝)

Tactic:
| add =>

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
⊢ f.inverse.domain = f.toFun.range

Tactic:
rw [inverse, Submodule.toLinearPMap_domain, ← graph_map_snd_eq_range,
    ← LinearEquiv.fst_comp_prodComm, Submodule.map_comp]

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

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
x : A[M]
⊢ ((domCongr R A e) x).coeff.support = Finset.map (↑e).toEmbedding x.coeff.support

Tactic:
by simp [domCongr, equivMapDomain]

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ ↑n ≤ p.degree

pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ p ≠ 0

Tactic:
· exact le_degree_of_ne_zero h

Goal state after:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ p ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ¬p.natDegree = 0 → p.coeff (p.natDegree - 1) = 0 ↔ ¬p.natDegree = 0 → ¬p.natDegree = 0 ∧ p.coeff (p.natDegree - 1) = 0

Tactic:
simp_all

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b ↦ (f b).degree
⊢ max (f a).degree (∑ i ∈ s, f i).degree ≤ (cons a s has).sup fun b ↦ (f b).degree

Tactic:
rw [sup_cons]; exact max_le_max le_rfl ih

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
⊢ p.natDegree = q.natDegree

pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : ¬p.natDegree = 0
⊢ p.natDegree = q.natDegree

Tactic:
on_goal 1 => by_cases h₂ : natDegree q = 0

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : q.natDegree = 0
⊢ p.natDegree = q.natDegree

case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : ¬q.natDegree = 0
⊢ p.natDegree = q.natDegree

case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : ¬p.natDegree = 0
⊢ p.natDegree = q.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
ha : ¬a = 0
⊢ ((monomial n) a).coeff (if a = 0 then 0 else n) = a

Tactic:
if_neg ha,

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
ha : ¬a = 0
⊢ ((monomial n) a).coeff n = a
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
by
  have : coeff p (natDegree q) = 0 := coeff_natDegree_eq_zero_of_degree_lt h
  simp only [leadingCoeff, natDegree_eq_of_degree_eq (degree_add_eq_right_of_degree_lt h), this,
    coeff_add, zero_add]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
ha : ¬a = 0
⊢ ((monomial n) a).leadingCoeff = a

Tactic:
rw [leadingCoeff, natDegree_monomial, if_neg ha, coeff_monomial]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
ha : ¬a = 0
⊢ (if n = n then a else 0) = a
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case neg.inl
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree = i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
simp_all

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.natDegree ≤ 0 ↔ p.degree ≤ 0

Tactic:
natDegree_le_iff_degree_le,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.degree ≤ ↑0 ↔ p.degree ≤ 0
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p₁ p₂ q₁ q₂ : R[X]
hp₁ : p₁ ≠ 0
hq₁ : q₁ ≠ 0
hp₂ : p₂ ≠ 0
hq₂ : q₂ ≠ 0
h_eq : p₁ * q₂ = p₂ * q₁
⊢ p₁.natDegree + q₂.natDegree = p₂.natDegree + q₁.natDegree

Tactic:
rw [← natDegree_mul hp₁ hq₂, ← natDegree_mul hp₂ hq₁, h_eq]

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
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst✝ : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
⊢ supDegree D (∑ j ∈ s, f j) = supDegree D (f i) ∧ leadingCoeff D (∑ j ∈ s, f j) = leadingCoeff D (f i)

Tactic:
by
  classical
  rw [← s.add_sum_erase _ hi]
  by_cases! hs : s.erase i = ∅
  · rw [hs, Finset.sum_empty, add_zero]; exact ⟨rfl, rfl⟩
  suffices _ from ⟨supDegree_add_eq_left this, leadingCoeff_add_eq_left this⟩
  refine supDegree_sum_lt ?_ (fun j hj => ?_)
  · exact hs
  · rw [Finset.mem_erase] at hj; exact hmax j hj.2 hj.1

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

Goal state before:
pp: R : Type u
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d).leadingCoeff = a

Tactic:
rw [add_assoc, add_assoc, ← add_assoc (C b * X ^ 2), add_comm,
    leadingCoeff_add_of_degree_lt <| degree_quadratic_lt_degree_C_mul_X_cb ha,
    leadingCoeff_C_mul_X_pow]

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:
by
  apply supDegree_eq_of_max
  · rw [← AddSubsemigroup.coe_set_mk (Set.range D), ← AddHom.srange_mk _ hadd, SetLike.mem_coe]
    · exact add_mem (supDegree_mem_range D hp) (supDegree_mem_range D hq)
    · exact (AddHom.srange ⟨D, hadd⟩).add_mem
  · simp_rw [Finsupp.mem_support_iff, coeff_supDegree_add_supDegree hD hadd]
    exact hpq
  · have := addLeftMono_of_addLeftStrictMono B
    have := addRightMono_of_addRightStrictMono B
    exact fun a ha => (Finset.le_sup ha).trans (supDegree_mul_le hadd)

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ ∑ n_1 ∈ p.support, ((C.comp f) (p.coeff n_1) * X ^ n_1).coeff n = f (p.coeff n)

Tactic:
simp_all

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
x a : A
h : a ∈ (aeval x).range
⊢ ∃ p, (aeval x) p = a

Tactic:
simp_all

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
x : A
a : ↥R[x]
y : A := ↑a
this : y ∈ (aeval x).range
h : y = ↑a
⊢ ∃ p, (aeval x) p = y

Tactic:
simp_all

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
t t' : R
⊢ algEquivAevalXAddC t = algEquivAevalXAddC t' ↔ t = t'

Tactic:
simp [algEquivAevalXAddC]

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
j : ι
a : β j
hj : ∀ (j_1 : ι), (fun x1 x2 ↦ x1 < x2) j_1 j → toLex x j_1 = toLex (update x j a) j_1
h : x j < update x j a j
⊢ x j < a

Tactic:
rwa [update_self] at h

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
j : ι
a : β j
hj : ∀ (j_1 : ι), (fun x1 x2 ↦ x1 < x2) j_1 j → toLex (update x j a) j_1 = toLex x j_1
h : update x j a j < x j
⊢ a < x j

Tactic:
rwa [update_self] at h

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
r : R
⊢ eval₂ f (f r) p = 0 → p.IsRoot r

Tactic:
intro h
  apply hf
  rw [← eval₂_hom, h, f.map_zero]

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

Goal state before:
pp: case tmul
R : Type u
S : Type v
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
k : ℕ
s : S
n : N
⊢ X ^ k • (rTensor N (↑R (monomial 0))) (s ⊗ₜ[R] n) = (rTensor N (↑R (monomial k))) (s ⊗ₜ[R] n)

Tactic:
| tmul s n =>

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

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f : Π₀ (a : α), N a
a✝ : α
⊢ f a✝ ≠ 0 a✝ ↔ f a✝ ≠ 0

Tactic:
Pi.zero_apply

Goal state after:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f : Π₀ (a : α), N a
a✝ : α
⊢ f a✝ ≠ 0 ↔ f a✝ ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → ℕ
t : Finset σ
⊢ ∀ x_1 ∈ t, x_1 ∉ (Finsupp.indicator t fun i x_2 ↦ x i).support → X x_1 ^ (Finsupp.indicator t fun i x_2 ↦ x i) x_1 = 1

Tactic:
intro i hi hi'

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → ℕ
t : Finset σ
i : σ
hi : i ∈ t
hi' : i ∉ (Finsupp.indicator t fun i x_1 ↦ x i).support
⊢ X i ^ (Finsupp.indicator t fun i x_1 ↦ x i) i = 1
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
i : σ
⊢ (if h : f i ∈ range f then X ((Equiv.ofInjective f hf).symm ⟨f i, h⟩) else 0) = X i

Tactic:
dif_pos ⟨i, rfl⟩,

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
i : σ
⊢ X ((Equiv.ofInjective f hf).symm ⟨f i, ⋯⟩) = X i
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case pos
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
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
n : σ →₀ ℕ
h : ¬coeff n p + coeff n q = 0
hp : coeff n p = 0
⊢ coeff n p ≠ 0 ∨ coeff n q ≠ 0

Tactic:
simp_all

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

Goal state before:
pp: case neg
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
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
n : σ →₀ ℕ
h : ¬coeff n p + coeff n q = 0
hp : ¬coeff n p = 0
⊢ coeff n p ≠ 0 ∨ coeff n q ≠ 0

Tactic:
simp_all

Goal state after:
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₁
ι : Type u_2
f : R →+* S₁
h : ι → MvPolynomial σ S₁
a✝ : R
⊢ eval₂ ((map f).comp C) h (C a✝) = eval₂ C h ((map f) (C a✝))

Tactic:
simp_all

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

Goal state before:
pp: case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
ι : Type u_2
f : R →+* S₁
h : ι → MvPolynomial σ S₁
p✝ q✝ : MvPolynomial ι R
a✝¹ : eval₂ ((map f).comp C) h p✝ = eval₂ C h ((map f) p✝)
a✝ : eval₂ ((map f).comp C) h q✝ = eval₂ C h ((map f) q✝)
⊢ eval₂ ((map f).comp C) h (p✝ + q✝) = eval₂ C h ((map f) (p✝ + q✝))

Tactic:
simp_all

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

Goal state before:
pp: case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
ι : Type u_2
f : R →+* S₁
h : ι → MvPolynomial σ S₁
p✝ : MvPolynomial ι R
n✝ : ι
a✝ : eval₂ ((map f).comp C) h p✝ = eval₂ C h ((map f) p✝)
⊢ eval₂ ((map f).comp C) h (p✝ * X n✝) = eval₂ C h ((map f) (p✝ * X n✝))

Tactic:
simp_all

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

Goal state before:
pp: case add
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
d : σ →₀ ℕ
p✝ q✝ : MvPolynomial σ R
a✝¹ : coeff (Finsupp.mapDomain f d) ((rename f) p✝) = coeff d p✝
a✝ : coeff (Finsupp.mapDomain f d) ((rename f) q✝) = coeff d q✝
⊢ coeff (Finsupp.mapDomain f d) ((rename f) (p✝ + q✝)) = coeff d (p✝ + q✝)

Tactic:
| add =>

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.degrees = 0
⊢ p.degrees.card = 0

Tactic:
simp_all

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

Goal state before:
pp: case refine_2.C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
a : S₁
hx : ↑(C a).coeffs ⊆ range ⇑f
⊢ C a ∈ range ⇑(map f)

Tactic:
by_cases h : a = 0
      · subst h
        exact ⟨0, by simp⟩
      · simp only [coeffs_C, h, reduceIte, Finset.coe_singleton, Set.singleton_subset_iff] at hx
        obtain ⟨b, rfl⟩ := hx
        exact ⟨C b, by simp⟩

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
hpq : Disjoint p.vars q.vars
⊢ (p - q).vars = p.vars ∪ q.vars

Tactic:
rw [← vars_neg q] at hpq
  convert! vars_add_of_disjoint hpq using 2 <;> simp [sub_eq_add_neg]

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

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

Tactic:
Pi.zero_apply

Goal state after:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
c : cons y s = 0
⊢ 0 = 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
⊢ (eval₂Hom f g) p = f (constantCoeff p)

Tactic:
conv_lhs => rw [p.as_sum]
  simp only [map_sum, eval₂Hom_monomial]
  by_cases h0 : constantCoeff p = 0
  on_goal 1 =>
    rw [h0, f.map_zero, Finset.sum_eq_zero]
    intro d hd
  on_goal 2 =>
    rw [Finset.sum_eq_single (0 : σ →₀ ℕ)]
    · rw [Finsupp.prod_zero_index, mul_one]
      rfl
    on_goal 1 => intro d hd hd0
  on_goal 3 =>
    rw [constantCoeff_eq, coeff, ← Ne, ← Finsupp.mem_support_iff] at h0
    intro
    contradiction
  repeat'
    obtain ⟨i, hi⟩ : Finset.Nonempty (Finsupp.support d) := by
      rw [constantCoeff_eq, coeff, ← Finsupp.notMem_support_iff] at h0
      rw [Finset.nonempty_iff_ne_empty, Ne, Finsupp.support_eq_empty]
      rintro rfl
      contradiction
    rw [Finsupp.prod, Finset.prod_eq_zero hi, mul_zero]
    rw [hp, zero_pow (Finsupp.mem_support_iff.1 hi)]
    rw [mem_vars_iff_mem_support]
    exact ⟨d, hd, hi⟩

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
⊢ degreesLE R σ (s + t) = degreesLE R σ s * degreesLE R σ t

Tactic:
le_antisymm_iff,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
⊢ degreesLE R σ (s + t) ≤ degreesLE R σ s * degreesLE R σ t ∧ degreesLE R σ s * degreesLE R σ t ≤ degreesLE R σ (s + t)
Module: Mathlib.Algebra.Polynomial.Degree.Monomial

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p = 0
h : p.natDegree = n.succ
⊢ False

Tactic:
simp_all

Goal state after: