mathlib-initiative/mathlib-tactics huggingface dataset:
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 : R
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
c x y : R
x✝¹ : x ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
x✝ : y ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ star c * x * c + star c * y * c ≤ star c * (x + y) * c

Tactic:
mul_add,

Goal state after:
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
c x y : R
x✝¹ : x ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
x✝ : y ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ star c * x * c + star c * y * c ≤ (star c * x + star c * y) * c
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: case mpr.add
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
x : A
hx : x ∈ S
y z : ↥(centralizer R S) ⊗[R] B
hy :
  includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y * includeLeft x
hz :
  includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z * includeLeft x
⊢ includeLeft x *
      ((Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y +
        (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z) =
    ((Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y +
        (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z) *
      includeLeft x

Tactic:
mul_add,

Goal state after:
case mpr.add
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
x : A
hx : x ∈ S
y z : ↥(centralizer R S) ⊗[R] B
hy :
  includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y * includeLeft x
hz :
  includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z * includeLeft x
⊢ includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y +
      includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z =
    ((Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y +
        (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z) *
      includeLeft x
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
⊢ ↥T →ₐ[R] B

Tactic:
by
  let compat :
      ∀ (i j) (x : A) (hxi : x ∈ (K i : Set A)) (hxj : x ∈ (K j : Set A)),
        f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩ := by
    intro i j x hxi hxj
    rcases dir i j with ⟨k, hik, hjk⟩
    simp [hf i k hik, hf j k hjk]
  let liftSup : ((iSup K : Subalgebra R A)) →ₐ[R] B :=
    { toFun :=
        Set.iUnionLift (fun i => ↑(K i)) (fun i x => f i x) compat
          ((iSup K : Subalgebra R A) : Set A)
          (le_of_eq <| coe_iSup_of_directed (K := K) dir)
      map_one' := by
        dsimp
        exact Set.iUnionLift_const _ (fun i : ι => (1 : K i)) (fun _ => rfl) _ (by simp)
      map_zero' := by
        dsimp
        exact Set.iUnionLift_const _ (fun i : ι => (0 : K i)) (fun _ => rfl) _ (by simp)
      map_mul' := by
        dsimp
        apply Set.iUnionLift_binary (coe_iSup_of_directed (K := K) dir) dir _ (fun _ => (· * ·))
        all_goals simp
      map_add' := by
        dsimp
        apply Set.iUnionLift_binary (coe_iSup_of_directed (K := K) dir) dir _ (fun _ => (· + ·))
        all_goals simp
      commutes' := fun r => by
        dsimp
        exact
          Set.iUnionLift_const _ (fun i : ι => algebraMap R (K i) r) (fun _ => rfl) _ (by simp) }
  exact liftSup.comp (inclusion hT)

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

Tactic:
exact ⟨r • a, smul_mem_closure_star_mul hr ha, add_smul ..⟩

Goal state after:
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
⊢ Module.rank R (ι →₀ M) = lift.{v, w} #ι * lift.{w, v} #fst✝

Tactic:
← (Finsupp.basis fun _ : ι => bs).mk_eq_rank'',

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
⊢ #((_ : ι) × fst✝) = lift.{v, w} #ι * lift.{w, v} #fst✝
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
inst✝ : Free R M
n : ℕ
h : Module.rank R M = ↑n
⊢ Module.Finite R M

Tactic:
by
  nontriviality R
  obtain ⟨⟨ι, b⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
  have := mk_lt_aleph0_iff.mp <|
    b.linearIndependent.cardinal_le_rank |>.trans_eq h |>.trans_lt natCast_lt_aleph0
  exact Module.Finite.of_basis b

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

Goal state before:
pp: 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)
j : n
⊢ Submodule.Quotient.mk ((bW.sumQuot bQ) (Sum.inr j)) = bQ j

Tactic:
by
  simpa only [sumQuot, Basis.coe_mk, Sum.elim_inr, Function.comp_apply, ← W.mkQ_apply]
    using Function.rightInverse_surjInv W.mkQ_surjective _

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
x : E
y : F
H✝ : ∀ (c : R), c • x = 0 → σ c • y = 0
H : ∀ (c₁ c₂ : R), c₁ • x = c₂ • x → σ c₁ • y = σ c₂ • y
c : R
z : ↥(R ∙ x)
this : ∀ (w : ↥(R ∙ x)), Classical.choose ⋯ • x = ↑w
⊢ Classical.choose ⋯ • x = (c * Classical.choose ⋯) • x

Tactic:
simp only [mul_smul, this]

Goal state after:
case a
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
x : E
y : F
H✝ : ∀ (c : R), c • x = 0 → σ c • y = 0
H : ∀ (c₁ c₂ : R), c₁ • x = c₂ • x → σ c₁ • y = σ c₂ • y
c : R
z : ↥(R ∙ x)
this : ∀ (w : ↥(R ∙ x)), Classical.choose ⋯ • x = ↑w
⊢ ↑(c • z) = c • ↑z
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
inst✝ : Free F E
a✝ : Nontrivial E
h : finrank F E = 1
⊢ Function.Surjective ⇑(algebraMap F E)

Tactic:
Algebra.surjective_algebraMap_iff,

Goal state after:
F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : StrongRankCondition F
inst✝² : Ring E
inst✝¹ : Algebra F E
inst✝ : Free F E
a✝ : Nontrivial E
h : finrank F E = 1
⊢ ⊤ = ⊥
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case e_a
R✝ : Type u_1
X : Type u_2
inst✝⁷ : CommSemiring R✝
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : SMul R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : R
s : S
x : FreeAlgebra A X
⊢ (r • s) • 1 = r • 1 * s • 1

Tactic:
smul_assoc,

Goal state after:
case e_a
R✝ : Type u_1
X : Type u_2
inst✝⁷ : CommSemiring R✝
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : SMul R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : R
s : S
x : FreeAlgebra A X
⊢ r • s • 1 = r • 1 * s • 1
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (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 => ?_⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥f.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑f z₁ = ↑(f.sup g h) z₂
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ (p * (X + ↑n)).comp q = p.comp q * (q + ↑n)

Tactic:
mul_add,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ (p * X + p * ↑n).comp q = p.comp q * (q + ↑n)
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
pos : 0 < n
np : n < 2
h1 : n = n.minFac
⊢ n.minFac ≤ n / n.minFac

Tactic:
le_antisymm (le_of_lt_succ np) (succ_le_of_lt pos),

Goal state after:
n : ℕ
pos : 0 < n
np : n < 2
h1 : n = n.minFac
⊢ minFac 1 ≤ 1 / minFac 1
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ x + y * 0 ≠ 0 ∧ x * 0 + y ≠ 0

Tactic:
mul_zero,

Goal state after:
R : Type u
inst✝ : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ x + 0 ≠ 0 ∧ 0 + y ≠ 0
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ x + y * 0 + z * 0 ≠ 0 ∧ x * 0 + y + z * 0 ≠ 0 ∧ x * 0 + y * 0 + z ≠ 0

Tactic:
mul_zero,

Goal state after:
R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ x + 0 + 0 ≠ 0 ∧ 0 + y + 0 ≠ 0 ∧ 0 + 0 + z ≠ 0
Module: Mathlib.Algebra.Polynomial.Coeff

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

Tactic:
(commute_X p).eq,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p * X).coeff (n + 1) = p.coeff n
Module: Mathlib.Algebra.Polynomial.Degree.Defs

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

Tactic:
degree_zero

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : p = 0
⊢ ⊥ ≤ q.degree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : Subsingleton R
⊢ degree 0 = ⊥

Tactic:
degree_zero

Goal state after:
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : Subsingleton R
⊢ ⊥ = ⊥
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
this : DecidableEq R := Classical.decEq R
h : a = 0
⊢ degree 0 ≤ ↑n

Tactic:
degree_zero

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
this : DecidableEq R := Classical.decEq R
h : a = 0
⊢ ⊥ ≤ ↑n
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
h : coeff 0 n ≠ 0
⊢ False

Tactic:
exact h rfl

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ (↑p.natDegree).succ = p.natDegree + 1

Tactic:
exact WithBot.succ_coe p.natDegree

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

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
⊢ C r ∣ φ → ∀ (i : ℕ), r ∣ φ.coeff i

pp: case mpr
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
⊢ (∀ (i : ℕ), r ∣ φ.coeff i) → C r ∣ φ

Tactic:
· rintro ⟨φ, rfl⟩ c
    rw [coeff_C_mul]
    apply dvd_mul_right

Goal state after:
case mpr
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
⊢ (∀ (i : ℕ), r ∣ φ.coeff i) → C r ∣ φ
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
by_contra h
  cases Nat.lt_or_lt_of_ne h with
  | inl h => exact lt_asymm h (by rwa [natDegree_add_eq_right_of_natDegree_lt h] at H)
  | inr h =>
    rw [natDegree_add_eq_left_of_natDegree_lt h] at H
    exact LT.lt.false H

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
a : WithBot ℕ
hp : p.degree ≤ a
n : ℕ
hn : (p ^ n).degree ≤ ↑n * a
⊢ (p ^ (n + 1)).degree ≤ ↑(n + 1) * a

Tactic:
Nat.cast_succ,

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
a : WithBot ℕ
hp : p.degree ≤ a
n : ℕ
hn : (p ^ n).degree ≤ ↑n * a
⊢ (p ^ (n + 1)).degree ≤ (↑n + 1) * a
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
mem_antidiagonal

Goal state after:
case refine_1
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)
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case refine_2
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p.natDegree, q.natDegree) ∉ antidiagonal (p.natDegree + q.natDegree)
⊢ (p.natDegree, q.natDegree) ∈ antidiagonal (p.natDegree + q.natDegree)

Tactic:
mem_antidiagonal

Goal state after:
case refine_2
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p.natDegree, q.natDegree) ∉ antidiagonal (p.natDegree + q.natDegree)
⊢ (p.natDegree, q.natDegree).1 + (p.natDegree, q.natDegree).2 = p.natDegree + q.natDegree
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: n m : WithBot ℕ
⊢ n + m = 0 ↔ n = 0 ∧ m = 0

Tactic:
cases n
  · simp [WithBot.bot_add]
  cases m
  · simp [WithBot.add_bot]
  simp [← WithBot.coe_add]

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
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ (p.coeff + q.coeff) (Function.invFun D (supDegree D p)) = leadingCoeff D p

Tactic:
Finsupp.add_apply,

Goal state after:
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
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ p.coeff (Function.invFun D (supDegree D p)) + q.coeff (Function.invFun D (supDegree D p)) = leadingCoeff D p
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : 0 ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn0 : p ^ n = 0
h1 : p.leadingCoeff ^ n ≠ 0
⊢ False

Tactic:
exact h rfl

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

Goal state before:
pp: case h
R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
⊢ (df, dg) ∈ antidiagonal (df + dg)

Tactic:
mem_antidiagonal

Goal state after:
case h
R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
⊢ (df, dg).1 + (df, dg).2 = df + dg
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_2
inst✝ : SMulZeroClass S R
a : S
p : R[X]
⊢ (a • p).degree ≤ p.degree

Tactic:
refine (degree_le_iff_coeff_zero _ _).2 fun m hm => ?_

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type u_2
inst✝ : SMulZeroClass S R
a : S
p : R[X]
m : ℕ
hm : p.degree < ↑m
⊢ (a • p).coeff m = 0
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).degree = ↑n

Tactic:
degree_X_pow

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
⊢ ↑n = ↑n
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hbot : ⊥ + ⊥ = ⊥
hp : Monic D p
hq : Monic D q
h✝ : Subsingleton R
⊢ supDegree D (0 * 0) = supDegree D 0 + supDegree D 0

Tactic:
mul_zero,

Goal state after:
case inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hbot : ⊥ + ⊥ = ⊥
hp : Monic D p
hq : Monic D q
h✝ : Subsingleton R
⊢ supDegree D 0 = supDegree D 0 + supDegree D 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case inr.inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder B
inst✝⁵ : OrderBot B
p : R[A]
D : A → B
inst✝⁴ : AddZeroClass A
inst✝³ : Add B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
⊢ leadingCoeff D (p * 0) = leadingCoeff D p * 0

Tactic:
mul_zero,

Goal state after:
case inr.inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder B
inst✝⁵ : OrderBot B
p : R[A]
D : A → B
inst✝⁴ : AddZeroClass A
inst✝³ : Add B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
⊢ leadingCoeff D 0 = 0
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ↑d.succ * (∑ x ∈ range d, ↑(d.choose x) * y ^ x + ↑(d.choose d) * y ^ d) - ↑d.succ * y ^ d =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))

Tactic:
mul_add,

Goal state after:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ↑d.succ * ∑ x ∈ range d, ↑(d.choose x) * y ^ x + ↑d.succ * (↑(d.choose d) * y ^ d) - ↑d.succ * y ^ d =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ∑ i ∈ range d, ↑d.succ * (↑(d.choose i) * y ^ i) =
    ∑ k ∈ range d, ↑((d + 1).choose (k + 1)) * (↑(k + 1) * y ^ (k + 1 - 1)) + ↑((d + 1).choose 0) * 0

Tactic:
mul_zero,

Goal state after:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ∑ i ∈ range d, ↑d.succ * (↑(d.choose i) * y ^ i) =
    ∑ k ∈ range d, ↑((d + 1).choose (k + 1)) * (↑(k + 1) * y ^ (k + 1 - 1)) + 0
Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
_hp : p ∈ ⊤
S : Subalgebra R R[X] := R[ X]
⊢ p ∈ S

Tactic:
rw [← sum_monomial_eq p]

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : R[X]
_hp : p ∈ ⊤
S : Subalgebra R R[X] := R[ X]
⊢ (p.sum fun n a ↦ (monomial n) a) ∈ S
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : p.Monic
h : ∀ (x : R), f x = 0
n : ℕ
⊢ (map f p).coeff n = coeff 0 n

Tactic:
simp only [h, coeff_map, coeff_zero]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ (map f p).degree ≤ p.degree

Tactic:
refine (degree_le_iff_coeff_zero _ _).2 fun m hm => ?_

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
m : ℕ
hm : p.degree < ↑m
⊢ (map f p).coeff m = 0
Module: Mathlib.Algebra.Polynomial.Eval.Degree

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

Tactic:
degree_zero

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : map f p = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ ⊥ = ⊥
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case pos
S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ ∑ n ∈ f.support, (RingHom.id S) (f.coeff n) * z ^ n
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
⊢ p ∣ f.coeff i * z ^ i

Tactic:
rw [← Finset.insert_erase hi, Finset.sum_insert (Finset.notMem_erase _ _)] at dvd_eval

Goal state after:
case pos
S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ (RingHom.id S) (f.coeff i) * z ^ i + ∑ x ∈ f.support.erase i, (RingHom.id S) (f.coeff x) * z ^ x
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
⊢ p ∣ f.coeff i * z ^ i
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
h : Decidable (a = 0)
⊢ ((monomial s) a).support = if a = 0 then ∅ else {s}

Tactic:
by
  rw [← Subsingleton.elim (Classical.decEq R a 0) h]
  rfl

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
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p : MvPolynomial σ R
⊢ (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) p

Tactic:
apply induction_on p
  · simp
  · intro p q hp hq
    simp [hp, hq]
  · intro p n hp
    simp [hp]

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

Goal state before:
pp: case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
⊢ C r ∣ φ → ∀ (i : σ →₀ ℕ), r ∣ coeff i φ

pp: case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
⊢ (∀ (i : σ →₀ ℕ), r ∣ coeff i φ) → C r ∣ φ

Tactic:
· rintro ⟨φ, rfl⟩ c
    rw [coeff_C_mul]
    apply dvd_mul_right

Goal state after:
case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
⊢ (∀ (i : σ →₀ ℕ), r ∣ coeff i φ) → C r ∣ φ