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✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
inst✝ : CompatibleSMul R S S S
x x✝¹ x✝ : S ⊗[R] S
hx : (includeLeft.comp (lmul'' R)) x✝¹ = (AlgHom.id S (S ⊗[R] S)) x✝¹
hy : (includeLeft.comp (lmul'' R)) x✝ = (AlgHom.id S (S ⊗[R] S)) x✝
⊢ (includeLeft.comp (lmul'' R)) (x✝¹ + x✝) = (AlgHom.id S (S ⊗[R] S)) (x✝¹ + x✝)

Tactic:
simp_all [add_tmul]

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Directed

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩ :=
  iSupLift._proof_2 K dir f hf
r : R
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ ((algebraMap R ↥(iSup K)) r) =
    (algebraMap R B) r

Tactic:
exact
          Set.iUnionLift_const _ (fun i : ι => algebraMap R (K i) r) (fun _ => rfl) _ (by simp)

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 : 0 ≤ r
a b : A
hab : a ≤ b
⊢ r • a ≤ r • b

Tactic:
rw [StarOrderedRing.nonneg_iff] at hr
    rw [StarOrderedRing.le_iff] at hab ⊢
    obtain ⟨a, ha, rfl⟩ := hab
    exact ⟨r • a, smul_mem_closure_star_mul hr ha, smul_add ..⟩

Goal state after:
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
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
⊢ LinearIndependent R (Sum.elim (fun x ↦ ↑(f x)) g)

Tactic:
refine .sum_type (hf.map' M'.subtype M'.ker_subtype) (.of_comp M'.mkQ hg) ?_
  refine disjoint_def.mpr fun x h₁ h₂ ↦ ?_
  have : x ∈ M' := span_le.mpr (Set.range_subset_iff.mpr fun i ↦ (f i).prop) h₁
  obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp h₂
  simp_rw [← Quotient.mk_eq_zero, ← mkQ_apply, map_finsuppSum, map_smul, mkQ_apply] at this
  rw [linearIndependent_iff.mp hg _ this, Finsupp.sum_zero_index]

Goal state after:
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
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
⊢ LinearIndependent R (Sum.elim (fun x ↦ ↑(f x)) g)

Tactic:
by
  refine .sum_type (hf.map' M'.subtype M'.ker_subtype) (.of_comp M'.mkQ hg) ?_
  refine disjoint_def.mpr fun x h₁ h₂ ↦ ?_
  have : x ∈ M' := span_le.mpr (Set.range_subset_iff.mpr fun i ↦ (f i).prop) h₁
  obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp h₂
  simp_rw [← Quotient.mk_eq_zero, ← mkQ_apply, map_finsuppSum, map_smul, mkQ_apply] at this
  rw [linearIndependent_iff.mp hg _ this, Finsupp.sum_zero_index]

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

Goal state before:
pp: R✝ : Type u_1
A : Type u_2
F : Type u_3
R : Type u_4
S : Type u_5
inst✝⁹ : NonUnitalSemiring R
inst✝⁸ : PartialOrder R
inst✝⁷ : StarRing R
inst✝⁶ : StarOrderedRing R
inst✝⁵ : NonUnitalSemiring S
inst✝⁴ : PartialOrder S
inst✝³ : StarRing S
inst✝² : StarOrderedRing S
inst✝¹ : EquivLike F R S
inst✝ : StarRingEquivClass F R S
f : F
x y : R
⊢ f x ≤ f y ↔ x ≤ y

Tactic:
refine ⟨fun h ↦ ?_, map_rel f⟩

Goal state after:
R✝ : Type u_1
A : Type u_2
F : Type u_3
R : Type u_4
S : Type u_5
inst✝⁹ : NonUnitalSemiring R
inst✝⁸ : PartialOrder R
inst✝⁷ : StarRing R
inst✝⁶ : StarOrderedRing R
inst✝⁵ : NonUnitalSemiring S
inst✝⁴ : PartialOrder S
inst✝³ : StarRing S
inst✝² : StarOrderedRing S
inst✝¹ : EquivLike F R S
inst✝ : StarRingEquivClass F R S
f : F
x y : R
h : f x ≤ f y
⊢ x ≤ y
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'
⊢ Nontrivial (V →ₗ[K] V')

Tactic:
by
  obtain ⟨v, hv⟩ := exists_ne (0 : V)
  obtain ⟨w, hw⟩ := exists_ne (0 : V')
  have : v ∉ (⊥ : Submodule K V) := by simp only [mem_bot, hv, not_false_eq_true]
  obtain ⟨g, _, hg⟩ := LinearMap.exists_extend_of_notMem (K := K) 0 this w
  exact ⟨g, 0, DFunLike.ne_iff.mpr ⟨v, by simp_all⟩⟩

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
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
have hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a := fun a ha b hb ↦
    Set.union_star_self_comm (fun _ ha _ hb ↦ hcomm _ hb _ ha)
      (fun _ ha _ hb ↦ hcomm_star _ hb _ ha) b hb a ha

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✝¹ : 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✝¹
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
s : Submodule K V
inst✝ : Free K ↥s
⊢ (∃ v₀, v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ r, r • v₀ = v) ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ r, r • v₀ = v

Tactic:
refine ⟨fun ⟨⟨v₀, hv₀⟩, H, h⟩ ↦ ⟨v₀, hv₀, fun h' ↦ by
    simp only [h', ne_eq] at H; exact H rfl, fun v hv ↦ ?_⟩,
    fun ⟨v₀, hv₀, H, h⟩ ↦ ⟨⟨v₀, hv₀⟩,
      fun h' ↦ H (by rwa [AddSubmonoid.mk_eq_zero] at h'), fun ⟨v, hv⟩ ↦ ?_⟩⟩

Goal state after:
case refine_1
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
x✝ : ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : ⟨v₀, hv₀⟩ ≠ 0
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
v : V
hv : v ∈ s
⊢ ∃ r, r • v₀ = v

case refine_2
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
x✝¹ : ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : v₀ ≠ 0
h : ∀ v ∈ s, ∃ r, r • v₀ = v
x✝ : ↥s
v : V
hv : v ∈ s
⊢ ∃ r, r • ⟨v₀, hv₀⟩ = ⟨v, hv⟩
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
⊢ n.minFacProp (n.minFacAux (x✝ + 2))

Tactic:
refine
        have := minFac_lemma n k h
        minFacAux_has_prop n2 (k + 2) (i + 1) (by simp [k, e, Nat.left_distrib, add_right_comm])
          fun m m2 d => ?_
      rcases Nat.eq_or_lt_of_le (a m m2 d) with rfl | ml
      · contradiction
      apply (Nat.eq_or_lt_of_le ml).resolve_left
      intro me
      rw [← me, e] at d
      have d' : 2 * (i + 2) ∣ n := d
      have := a _ le_rfl (dvd_of_mul_right_dvd d')
      rw [e] at this
      exact absurd this (by contradiction)

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

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

Tactic:
simp [hy, hx']

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: 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 : E →ₗ.[R] F
x_fst : E
x_snd : F
fst✝ : E
snd✝ : F
h : fst✝ = x_fst ∧ -snd✝ = x_snd
y : ↥f.domain
hy : ↑y = (fst✝, snd✝).1
hx' : ↑f y = (fst✝, snd✝).2
⊢ ↑y = (fst✝, -snd✝).1 ∧ ↑(-f) y = (fst✝, -snd✝).2

Tactic:
simp [hy, hx']

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

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ico b a)
⊢ IsMaxOn f (Iio a) b

Tactic:
by
  intro x hx
  by_cases! g₀ : x ≤ b
  · exact h₀ g₀ self_mem_Iic g₀
  · exact h₁ (left_mem_Ico.2 (g₀.trans hx)) ⟨g₀.le, hx⟩ g₀.le

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.natDegree < n
⊢ p.coeff n = 0

Tactic:
apply coeff_eq_zero_of_degree_lt
  by_cases hp : p = 0
  · subst hp
    exact WithBot.bot_lt_coe n
  · rwa [degree_eq_natDegree hp, Nat.cast_lt]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.degree < p.degree
⊢ p.coeff p.natDegree ≠ 0

Tactic:
exact mt leadingCoeff_eq_zero.1 (ne_zero_of_degree_gt h)

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

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

Tactic:
exact leadingCoeff_add_of_degree_lt h

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
hp : ¬p = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
rwa [hq.leadingCoeff, mul_one, Ne, leadingCoeff_eq_zero]

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

Goal state before:
pp: case neg.refine_2
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)
hs : (s.erase i).Nonempty
j : ι
hj : j ∈ s.erase i
⊢ supDegree D (f j) < supDegree D (f i)

Tactic:
rw [Finset.mem_erase] at hj

Goal state after:
case neg.refine_2
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)
hs : (s.erase i).Nonempty
j : ι
hj : j ≠ i ∧ j ∈ s
⊢ supDegree D (f j) < supDegree D (f i)
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
replace hlc : leadingCoeff p + leadingCoeff (-q) ≠ 0 := by
    rwa [← sub_ne_zero, sub_eq_add_neg, ← q.leadingCoeff_neg] at hlc

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

Goal state before:
pp: R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
a : R
this : (C a).degree < X.degree
⊢ (X + C a).degree = 1

Tactic:
degree_add_eq_left_of_degree_lt this,

Goal state after:
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
a : R
this : (C a).degree < X.degree
⊢ X.degree = 1
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
this : (C a).degree < (X ^ n).degree
⊢ (X ^ n + C a).degree = ↑n

Tactic:
degree_add_eq_left_of_degree_lt this,

Goal state after:
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
this : (C a).degree < (X ^ n).degree
⊢ (X ^ n).degree = ↑n
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 1 ≤ a
hb : 1 ≤ b
⊢ 1 ≤ if p then a else b

Tactic:
by split <;> assumption

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : a ≤ 1
hb : b ≤ 1
⊢ (if p then a else b) ≤ 1

Tactic:
by split <;> assumption

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 1 < a
hb : 1 < b
⊢ 1 < if p then a else b

Tactic:
by split <;> assumption

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : a < 1
hb : b < 1
⊢ (if p then a else b) < 1

Tactic:
by split <;> assumption

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

Goal state before:
pp: case refine_1
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
x✝ : ∃ a b, a + b = y ∧ embDomain f a = u ∧ embDomain f b = v
w z : α →₀ ℕ
h : w + z = y
hw : embDomain f w = u
hz : embDomain f z = v
⊢ embDomain f w + v = embDomain f y

Tactic:
← hz,

Goal state after:
case refine_1
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
x✝ : ∃ a b, a + b = y ∧ embDomain f a = u ∧ embDomain f b = v
w z : α →₀ ℕ
h : w + z = y
hw : embDomain f w = u
hz : embDomain f z = v
⊢ embDomain f w + embDomain f z = embDomain f y
Module: Mathlib.Algebra.Polynomial.AlgebraMap

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

Tactic:
by
  conv_rhs => rw [← Polynomial.sum_C_mul_X_pow_eq p]
  simp only [eval₂_eq_sum, sum_def]
  simp only [map_sum, map_mul, map_pow]
  simp [Polynomial.C_eq_algebraMap]

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 = (φ.comp (AlgHom.id R R[X])) p

Tactic:
AlgHom.comp_id

Goal state after:
R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
φ : R[X] →ₐ[R] A
p : R[X]
⊢ φ p = φ p
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
r : R
x✝ : IsUnit (X - C r)
g : R[X]
_hfg : (X - C r) * g = 1
hgf : g * (X - C r) = 1
⊢ 0 = 1

Tactic:
by rw [← eval_mul_X_sub_C, hgf, eval_one]

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

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

Tactic:
suffices (P * Q).coeff (l + m) = P.coeff l * Q.leadingCoeff by rw [← this, hQ, coeff_zero]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
⊢ (eval (⇑(eval g) ∘ f)) p = (eval g) (eval₂ C f p)

Tactic:
eval₂_comp_left (eval g)

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
⊢ (eval (⇑(eval g) ∘ f)) p = eval₂ ((eval g).comp C) (⇑(eval g) ∘ f) p
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₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p✝ p q : MvPolynomial σ R
hp : k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p)
hq : k (eval₂ f g q) = eval₂ k (⇑k ∘ g) ((map f) q)
⊢ k (eval₂ f g p) + k (eval₂ f g q) = eval₂ k (⇑k ∘ g) ((map f) (p + q))

Tactic:
(map f).map_add,

Goal state after:
case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p✝ p q : MvPolynomial σ R
hp : k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p)
hq : k (eval₂ f g q) = eval₂ k (⇑k ∘ g) ((map f) q)
⊢ k (eval₂ f g p) + k (eval₂ f g q) = eval₂ k (⇑k ∘ g) ((map f) p + (map f) q)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
n : σ
inst✝ : CommSemiring R
P Q : MvPolynomial σ R
hPQ : X n * P = X n * Q
i : σ →₀ ℕ
⊢ coeff (Finsupp.single n 1 + i) (X n * Q) = coeff i Q

Tactic:
coeff_X_mul i n Q

Goal state after:
R : Type u
σ : Type u_1
n : σ
inst✝ : CommSemiring R
P Q : MvPolynomial σ R
hPQ : X n * P = X n * Q
i : σ →₀ ℕ
⊢ coeff i Q = coeff i Q
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case add
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p q : MvPolynomial S₂ R
hp : (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p)
hq : (map f) (eval₂ C g q) = eval₂ C (⇑(map f) ∘ g) ((map f) q)
⊢ (map f) (eval₂ C g p + eval₂ C g q) = eval₂ C (⇑(map f) ∘ g) ((map f) (p + q))

Tactic:
(map f).map_add,

Goal state after:
case add
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p q : MvPolynomial S₂ R
hp : (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p)
hq : (map f) (eval₂ C g q) = eval₂ C (⇑(map f) ∘ g) ((map f) q)
⊢ (map f) (eval₂ C g p) + (map f) (eval₂ C g q) = eval₂ C (⇑(map f) ∘ g) ((map f) (p + q))
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case add
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p q : MvPolynomial S₂ R
hp : (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p)
hq : (map f) (eval₂ C g q) = eval₂ C (⇑(map f) ∘ g) ((map f) q)
⊢ eval₂ C (⇑(map f) ∘ g) ((map f) p) + eval₂ C (⇑(map f) ∘ g) ((map f) q) = eval₂ C (⇑(map f) ∘ g) ((map f) (p + q))

Tactic:
(map f).map_add,

Goal state after:
case add
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p q : MvPolynomial S₂ R
hp : (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p)
hq : (map f) (eval₂ C g q) = eval₂ C (⇑(map f) ∘ g) ((map f) q)
⊢ eval₂ C (⇑(map f) ∘ g) ((map f) p) + eval₂ C (⇑(map f) ∘ g) ((map f) q) =
    eval₂ C (⇑(map f) ∘ g) ((map f) p + (map f) q)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ constantCoeff.comp C = RingHom.id R

Tactic:
ext x
  exact constantCoeff_C σ x

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₁
x : MvPolynomial σ S₁
⊢ x ∈ range ⇑(map f) ↔ ↑x.coeffs ⊆ range ⇑f

Tactic:
by
  classical
  refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
  · obtain ⟨p, rfl⟩ := hx
    exact subset_trans (coe_coeffs_map f p) (by simp)
  · induction x using induction_on'' with
    | C a =>
      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⟩
    | mul_X p n ih =>
      rw [coeffs_mul_X] at hx
      obtain ⟨q, rfl⟩ := ih hx
      exact ⟨q * X n, by simp⟩
    | monomial_add a s p ha hs hp ih =>
      rw [coeffs_add (disjoint_support_monomial ha hs)] at hx
      simp only [Finset.coe_union, Set.union_subset_iff] at hx
      obtain ⟨q, hq⟩ := ih hx.1
      obtain ⟨u, hu⟩ := hp hx.2
      exact ⟨q + u, by simp [hq, hu]⟩

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

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

pp: case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h✝ : degreeOf i p ≠ degreeOf i q
h : degreeOf i q < degreeOf i p
⊢ max (degreeOf i p) (degreeOf i q) ≤ degreeOf i (p + q)

Tactic:
· simp [add_comm p q, degreeOf_add_eq_of_degreeOf_lt h, max_eq_right_of_lt h]

Goal state after:
case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h✝ : degreeOf i p ≠ degreeOf i q
h : degreeOf i q < degreeOf i p
⊢ max (degreeOf i p) (degreeOf i q) ≤ degreeOf i (p + q)
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
q : S[X]
h : p.trailingDegree = q.trailingDegree
⊢ p.natTrailingDegree = q.natTrailingDegree

Tactic:
by
  unfold natTrailingDegree
  rw [h]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree

Tactic:
exact le_trailingDegree_mul

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : g = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
g0,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : g = 0
⊢ reflect (N + O) (f * 0) = reflect N f * reflect O 0