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

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T✝ : Type u_2
A✝ : Type uA
B✝ : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝³² : CommSemiring R
inst✝³¹ : CommSemiring S
inst✝³⁰ : Algebra R S
inst✝²⁹ : Semiring A✝
inst✝²⁸ : Algebra R A✝
inst✝²⁷ : Algebra S A✝
inst✝²⁶ : IsScalarTower R S A✝
inst✝²⁵ : Semiring B✝
inst✝²⁴ : Algebra R B✝
inst✝²³ : Semiring C
inst✝²² : Algebra R C
inst✝²¹ : Algebra S C
inst✝²⁰ : IsScalarTower R S C
inst✝¹⁹ : Semiring D
inst✝¹⁸ : Algebra R D
inst✝¹⁷ : Semiring E
inst✝¹⁶ : Algebra R E
inst✝¹⁵ : Algebra S E
inst✝¹⁴ : IsScalarTower R S E
inst✝¹³ : Semiring F
inst✝¹² : Algebra R F
T : Type u_3
A : Type u_4
B : Type u_5
inst✝¹¹ : CommSemiring T
inst✝¹⁰ : CommSemiring A
inst✝⁹ : CommSemiring B
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra T A
inst✝⁴ : IsScalarTower R T A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : Algebra S T
inst✝ : IsScalarTower S T A
⊢ (AlgebraTensorModule.cancelBaseChange R S T A B).symm 1 = 1

Tactic:
by simp [Algebra.TensorProduct.one_def]

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

Goal state before:
pp: A : Type u_1
𝕜 : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : PartialOrder A
inst✝⁴ : ZeroLEOneClass A
inst✝³ : Semifield 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Algebra 𝕜 A
inst✝ : PosSMulMono 𝕜 A
c : 𝕜
hc : 0 < c
⊢ IsStrictlyPositive ((algebraMap 𝕜 A) c)

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Goal state after:
A : Type u_1
𝕜 : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : PartialOrder A
inst✝⁴ : ZeroLEOneClass A
inst✝³ : Semifield 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Algebra 𝕜 A
inst✝ : PosSMulMono 𝕜 A
c : 𝕜
hc : 0 < c
⊢ IsStrictlyPositive (c • 1)
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a c p : R
hp : 0 ≤ p
⊢ ∃ p_1, 0 ≤ p_1 ∧ star c * (a + p) * c = star c * a * c + p_1

Tactic:
exact ⟨star c * p * c, star_left_conjugate_nonneg hp c, by simp only [add_mul, mul_add]⟩

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
this : 0 ≤ x * star u * star v
⊢ 0 ≤ x

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
this : 0 ≤ x * (star u * star v)
⊢ 0 ≤ x
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
⊢ (⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R M

Tactic:
Cardinal.ciSup_add_ciSup _ bddAbove_of_small _ bddAbove_of_small

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
⊢ ⨆ i, ⨆ j, #↑↑i + #↑↑j ≤ Module.rank R M
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
⊢ (⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R (M × M₁)

Tactic:
Cardinal.ciSup_add_ciSup _ bddAbove_of_small _ bddAbove_of_small

Goal state after:
R : Type u
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
⊢ ⨆ i, ⨆ j, #↑↑i + #↑↑j ≤ Module.rank R (M × M₁)
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Free R M
ι : Type w
fst✝ : Type v
bs : Basis fst✝ R M
⊢ (sum fun i ↦ #fst✝) = lift.{v, w} #ι * lift.{w, v} #fst✝

Tactic:
Cardinal.sum_const

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Free R M
ι : Type w
fst✝ : Type v
bs : Basis fst✝ R M
⊢ lift.{v, w} #ι * lift.{w, v} #fst✝ = lift.{v, w} #ι * lift.{w, v} #fst✝
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: case intro.intro
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : StrongRankCondition R
inst✝² : Free R M
m : Type w
n : Type w'
inst✝¹ : Finite m
inst✝ : Finite n
val✝¹ : Fintype m
val✝ : Fintype n
I : Type v
b : Basis I R M
⊢ #(m × n × I) = lift.{max v w', w} #m * lift.{max v w, w'} #n * lift.{max w w', v} (Module.rank R M)

Tactic:
simp only [mk_prod, lift_mul, lift_lift, ← mul_assoc, b.mk_eq_rank'']

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✝¹¹ : 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
p q : NonUnitalStarSubalgebra R A
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ p = q

Tactic:
cases p; cases q; congr; exact SetLike.coe_injective h

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

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
S : Subalgebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥S
⊢ Module.rank F ↥S = 1 ↔ S = ⊥

Tactic:
refine ⟨fun h ↦ Subalgebra.eq_bot_of_rank_le_one h.le, ?_⟩
  rintro rfl
  obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := F) (M := (⊥ : Subalgebra F E))
  refine le_antisymm ?_ ?_
  · have := lift_rank_range_le (Algebra.linearMap F E)
    rwa [← one_eq_range, rank_self, lift_one, lift_le_one_iff,
      ← Algebra.toSubmodule_bot, rank_toSubmodule] at this
  · by_contra H
    rw [not_le, Cardinal.lt_one_iff] at H
    have := mk_eq_zero_iff.1 (H ▸ b.mk_eq_rank'')
    have := b.repr.toEquiv.subsingleton
    exact one_ne_zero congr((⊥ : Subalgebra F E).val $(Subsingleton.elim 1 0))

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
⊢ (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) t = F t

Tactic:
rcases t with ⟨x⟩

Goal state after:
case mk
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
x : Pre R X
⊢ (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) x) = F (Quot.mk (Rel R X) x)
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk.add
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha : (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) a) = F (Quot.mk (Rel R X) a)
hb : (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) b) = F (Quot.mk (Rel R X) b)
fa : FreeAlgebra R X := Quot.mk (Rel R X) a
fb : FreeAlgebra R X := Quot.mk (Rel R X) b
⊢ (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) (a.add b)) = F (Quot.mk (Rel R X) (a.add b))

Tactic:
change liftAux R (F ∘ ι R) (fa + fb) = F (fa + fb)

Goal state after:
case mk.add
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha : (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) a) = F (Quot.mk (Rel R X) a)
hb : (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) b) = F (Quot.mk (Rel R X) b)
fa : FreeAlgebra R X := Quot.mk (Rel R X) a
fb : FreeAlgebra R X := Quot.mk (Rel R X) b
⊢ (liftAux R (⇑F ∘ ι R)) (fa + fb) = F (fa + fb)
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
⊢ ringChar R ∣ 1 ↔ Subsingleton R

Tactic:
← spec,

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
⊢ ↑1 = 0 ↔ Subsingleton R
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 / n.minFac

Tactic:
conv_rhs =>
      congr
      rw [hx]

Goal state after:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
⊢ n.minFac ≤ n.minFac * (x + 2) / n.minFac
Module: Mathlib.Algebra.Polynomial.Coeff

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

Tactic:
← C_mul_X_pow_eq_monomial,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
r : R
⊢ (p * (C r * X ^ n)).coeff (d + n) = p.coeff d * r
Module: Mathlib.Algebra.Polynomial.Coeff

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

Tactic:
← C_mul_X_pow_eq_monomial,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
r : R
⊢ (C r * X ^ n * p).coeff (d + n) = r * p.coeff d
Module: Mathlib.Algebra.Polynomial.Coeff

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

Tactic:
mul_assoc,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
r : R
⊢ (C r * (X ^ n * p)).coeff (d + n) = r * p.coeff d
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R' : Type u_2
A : Type u_3
B : Type u_5
inst✝² : Ring R'
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
f g : R'[A]
⊢ supDegree D (f + -g) ≤ supDegree D f ⊔ supDegree D (-g)

Tactic:
apply supDegree_add_le

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✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
p : R[A]
a : A
hlt : ¬D a ≤ supDegree D p
⊢ p.coeff a = 0

Tactic:
contrapose! hlt

Goal state after:
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
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
i : ℕ
r : R
hr : ¬r = 0
⊢ ((monomial i) r).natDegree = i

Tactic:
← C_mul_X_pow_eq_monomial,

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
i : ℕ
r : R
hr : ¬r = 0
⊢ (C r * X ^ i).natDegree = i
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: case neg.p1
R : Type u
inst✝⁴ : Semiring R
p : R[X]
S : Type u_1
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : Module S R
inst✝ : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : ¬p = 0
⊢ a • p.coeff p.natDegree ≠ 0

Tactic:
apply smul_ne_zero ha

Goal state after:
case neg.p1
R : Type u
inst✝⁴ : Semiring R
p : R[X]
S : Type u_1
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : Module S R
inst✝ : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : ¬p = 0
⊢ p.coeff p.natDegree ≠ 0
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
⊢ (p ^ n).natDegree = n * p.natDegree

Tactic:
rw [hp0, 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.Operations

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : ¬p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff

Tactic:
← natDegree_pow' hp1,

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : ¬p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff ((p ^ i).natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ha : a ≠ 0
hp : IsRightRegular p.leadingCoeff
⊢ ¬a * p.leadingCoeff = 0

Tactic:
exact hp.mul_right_eq_zero_iff.ne.mpr ha

Goal state after:
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
hlc : p.leadingCoeff ≠ q.leadingCoeff
⊢ (p - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff

Tactic:
replace h : degree p = degree (-q) := by rwa [q.degree_neg]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hlc : p.leadingCoeff ≠ q.leadingCoeff
h : p.degree = (-q).degree
⊢ (p - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
⊢ (map f p).leadingCoeff = f p.leadingCoeff

Tactic:
by
  unfold leadingCoeff
  rw [coeff_map, natDegree_map_of_leadingCoeff_ne_zero f hf]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
⊢ IsUnit (f.coeff 0)

Tactic:
convert! hf

Goal state after:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
⊢ f.coeff 0 = f.leadingCoeff
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : IsEmpty σ
p : MvPolynomial σ R
⊢ C (p.coeff 0) = p

Tactic:
by apply AddMonoidAlgebra.ext; ext; simp [C_apply, ← single_eq_monomial]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
a : R
⊢ C a * X s = (monomial (Finsupp.single s 1)) a

Tactic:
← C_mul_X_pow_eq_monomial,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
a : R
⊢ C a * X s = C a * X s ^ 1
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ Algebra.adjoin R (range X) = ⊤

Tactic:
set S := Algebra.adjoin R (range (X : σ → MvPolynomial σ R))

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
⊢ S = ⊤
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
⊢ eval₂ f g₁ p = eval₂ f g₂ p

Tactic:
by
  apply Finset.sum_congr rfl
  intro C hc; dsimp; congr 1
  apply Finset.prod_congr rfl
  intro i hi; dsimp; congr 1
  apply h hi
  rwa [Finsupp.mem_support_iff] at hc

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p✝ p : MvPolynomial σ R
n : σ
hp : (map f) ((rename g) p) = (rename g) ((map f) p)
⊢ (map f) ((rename g) (p * X n)) = (rename g) ((map f) (p * X n))

Tactic:
simp only [hp, rename_X, map_X, map_mul]

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

Goal state before:
pp: case neg
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
u : τ →₀ ℕ
r : R
h : ¬↑u.support ⊆ range f
⊢ u = Finsupp.mapDomain f s → 0 = r

Tactic:
intro rfl

Goal state after:
case neg
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
r : R
h : ¬↑(Finsupp.mapDomain f s).support ⊆ range f
⊢ 0 = r
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: 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
⊢ eval₂ ((map f).comp C) h p = eval₂ C h ((map f) p)

Tactic:
induction p using MvPolynomial.induction_on

Goal state after:
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✝))

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✝))

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✝))
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∑ i ∈ p.support, ((monomial i) (coeff i p)).coeff = p.coeff

Tactic:
exact Finsupp.sum_single _

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

Goal state before:
pp: case h.left
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial (↥s₁) R
s₂ : Finset σ
q₂ : MvPolynomial (↥s₂) R
⊢ (rename Subtype.val) q₁ = (rename Subtype.val) ((rename fun x ↦ ⟨↑x, ⋯⟩) q₁)

Tactic:
simp [Function.comp_def]

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

Goal state before:
pp: case h.right
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial (↥s₁) R
s₂ : Finset σ
q₂ : MvPolynomial (↥s₂) R
⊢ (rename Subtype.val) q₂ = (rename Subtype.val) ((rename fun x ↦ ⟨↑x, ⋯⟩) q₂)

Tactic:
simp [Function.comp_def]

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₁
q : R →+* S₁
r : R
hr : ∀ (r' : R), q r' = 0 ↔ r ∣ r'
φ : MvPolynomial σ R
⊢ C r ∣ φ ↔ (map q) φ = 0

Tactic:
by
  rw [C_dvd_iff_dvd_coeff, MvPolynomial.ext_iff]
  simp only [coeff_map, coeff_zero, hr]

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

Goal state before:
pp: case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
x : MvPolynomial σ S
hx : x ∈ coeffsIn σ M
y : MvPolynomial σ S
hy : y ∈ coeffsIn σ N
k : σ →₀ ℕ
⊢ ∑ x_1 ∈ Finset.antidiagonal k, coeff x_1.1 x * coeff x_1.2 y ∈ M * N

Tactic:
exact sum_mem fun c hc ↦ Submodule.mul_mem_mul (hx _) (hy _)

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 : σ
s : σ →₀ ℕ
h : s ∈ p.support
⊢ s i ≤ degreeOf i p

Tactic:
obtain si | si := eq_or_lt_of_le <| Nat.zero_le (s i)
  · simp [← si]
  rw [degreeOf_eq_sup, Finset.le_sup_iff si]
  use s

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

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

Tactic:
have : p * X i ^ k ≠ 0 := by
      rcases ne_zero_iff.mp h with ⟨s, hs⟩
      refine ne_zero_iff.mpr ⟨s + Finsupp.single i k, ?_⟩
      rwa [X_pow_eq_monomial, coeff_mul_monomial, mul_one]

Goal state after:
case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * X i ^ k) = degreeOf i p + k
this : p * X i ^ k ≠ 0
⊢ degreeOf i (p * X i ^ (k + 1)) = degreeOf i p + (k + 1)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
⊢ degreeOf i (p + q) ≤ degreeOf i p

Tactic:
rw [← max_eq_left_of_lt h]
    exact degreeOf_add_le i p q

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

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
i : σ
⊢ degreeOf (f i) ((rename f) p) = degreeOf i p

Tactic:
simp only [degreeOf, degrees_rename_of_injective h, Multiset.count_map_eq_count' f p.degrees h]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
⊢ ((monomial s) c).totalDegree ≤ s.sum fun x ↦ id

Tactic:
if hc : c = 0 then
    simp only [hc, map_zero, totalDegree_zero, zero_le]
  else
    rw [totalDegree_monomial _ hc, Function.id_def]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
h₁ : c = 0
⊢ #f.eraseLead.support + 1 = 0

Tactic:
by_contra
    exact h (card_support_eq_zero.mp h₁)

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

Goal state before:
pp: R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
⊢ (s.sum f).degree = s.sup fun i ↦ (f i).degree

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert x s hx IH =>
    simp only [hx, Finset.sum_insert, not_false_iff, Finset.sup_insert]
    specialize IH (h.mono fun _ => by simp +contextual)
    rcases lt_trichotomy (degree (f x)) (degree (s.sum f)) with (H | H | H)
    · rw [← IH, sup_eq_right.mpr H.le, degree_add_eq_right_of_degree_lt H]
    · rcases s.eq_empty_or_nonempty with (rfl | hs)
      · simp
      obtain ⟨y, hy, hy'⟩ := Finset.exists_mem_eq_sup s hs fun i => degree (f i)
      rw [IH, hy'] at H
      by_cases hx0 : f x = 0
      · simp [hx0, IH]
      have hy0 : f y ≠ 0 := by
        contrapose! H
        simpa [H, degree_eq_bot] using hx0
      refine absurd H (h ?_ ?_ fun H => hx ?_)
      · simp [hx0]
      · simp [hy, hy0]
      · exact H.symm ▸ hy
    · rw [← IH, sup_eq_left.mpr H.le, degree_add_eq_left_of_degree_lt H]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : n = p.natDegree
⊢ (p + q).eraseLead.coeff p.natDegree = (p.eraseLead + q).coeff p.natDegree

Tactic:
eraseLead_coeff,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : n = p.natDegree
⊢ (if p.natDegree = (p + q).natDegree then 0 else (p + q).coeff p.natDegree) = (p.eraseLead + q).coeff p.natDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
⊢ (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n

Tactic:
eraseLead_coeff,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
⊢ (if n = (p + q).natDegree then 0 else (p + q).coeff n) = (p.eraseLead + q).coeff n
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
⊢ (if n = (p + q).natDegree then 0 else p.coeff n + q.coeff n) = p.eraseLead.coeff n + q.coeff n

Tactic:
eraseLead_coeff,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
⊢ (if n = (p + q).natDegree then 0 else p.coeff n + q.coeff n) = (if n = p.natDegree then 0 else p.coeff n) + q.coeff n