mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Algebra.Spectrum.Pi

Goal state before:
pp: A : Type u_2
B : Type u_3
R : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
a : A
b : B
⊢ (resolventSet R (a, b))ᶜᶜ = ((resolventSet R a)ᶜ ∪ (resolventSet R b)ᶜ)ᶜ

Tactic:
Set.compl_union,

Goal state after:
A : Type u_2
B : Type u_3
R : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
a : A
b : B
⊢ (resolventSet R (a, b))ᶜᶜ = (resolventSet R a)ᶜᶜ ∩ (resolventSet R b)ᶜᶜ
Module: Mathlib.Algebra.Algebra.StrictPositivity

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

Tactic:
Units.isUnit_units_mul

Goal state after:
A : Type u_1
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
u : Aˣ
⊢ 0 ≤ a ∧ IsUnit a ↔ 0 ≤ a ∧ IsUnit a
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
ι : 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
i : ι
x : ↥(K i)
h : K i ≤ T
⊢ (iSupLift K dir f hf T hT) ((inclusion h) x) = (f i) x

Tactic:
dsimp [iSupLift, inclusion]

Goal state after:
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
ι : 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
i : ι
x : ↥(K i)
h : K i ≤ T
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ ⟨↑x, ⋯⟩ = (f i) 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
ι : 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
i : ι
x : ↥(K i)
hx : ↑x ∈ T
⊢ (iSupLift K dir f hf T hT) ⟨↑x, hx⟩ = (f i) x

Tactic:
dsimp [iSupLift, inclusion]

Goal state after:
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
ι : 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
i : ι
x : ↥(K i)
hx : ↑x ∈ T
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ ⟨↑x, ⋯⟩ = (f i) x
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: case e'_1
R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : Rᵐᵒᵖ
p : R
⊢ p ∈ AddSubmonoid.comap opAddEquiv (AddSubmonoid.map opAddEquiv (AddSubmonoid.closure (range fun s ↦ star s * s))) ↔
    op p ∈ AddSubmonoid.closure (range fun s ↦ star s * s)

pp: case e'_2
R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : Rᵐᵒᵖ
p : R
⊢ unop y = unop x + p ↔ y = x + op p

Tactic:
· simp [AddMonoidHom.map_mclosure, ← range_comp', Function.comp_def,
        ← (star_involutive.surjective.comp op_surjective).range_comp]

Goal state after:
case e'_2
R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : Rᵐᵒᵖ
p : R
⊢ unop y = unop x + p ↔ y = x + op p
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
ι : 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
i : ι
x : ↥T
hx : ↑x ∈ K i
⊢ (iSupLift K dir f hf T hT) x = (f i) ⟨↑x, hx⟩

Tactic:
dsimp [iSupLift, inclusion]

Goal state after:
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
ι : 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
i : ι
x : ↥T
hx : ↑x ∈ K i
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ (Set.inclusion hT x) = (f i) ⟨↑x, hx⟩
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: case hli
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 := ⋯
br : ⇑W.mkQ ∘ b ∘ Sum.inr = ⇑bQ
⊢ LinearIndependent R b

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 := ⋯
br : ⇑W.mkQ ∘ b ∘ Sum.inr = ⇑bQ
⊢ ⊤ ≤ span R (range b)

Tactic:
· apply LinearIndependent.sumElim_of_quotient
    · exact bW.linearIndependent
    · convert! bQ.linearIndependent

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 := ⋯
br : ⇑W.mkQ ∘ b ∘ Sum.inr = ⇑bQ
⊢ ⊤ ≤ span R (range b)
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: ι : Type w
R : Type u
M : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
this : lift.{v, w} #{ i // p i ≠ ⊥ } ≤ lift.{v, w} ↑(finrank R M)
⊢ #{ i // p i ≠ ⊥ } ≤ ↑(finrank R M)

Tactic:
Cardinal.lift_le

Goal state after:
ι : Type w
R : Type u
M : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
this : #{ i // p i ≠ ⊥ } ≤ ↑(finrank R M)
⊢ #{ i // p i ≠ ⊥ } ≤ ↑(finrank R M)
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
⊢ ∃ c, c • x = y

Tactic:
have : Submodule.span K {x} = ⊤ := by
    have : FiniteDimensional K V := .of_finrank_eq_succ h
    apply eq_top_of_finrank_eq
    rw [h]
    exact finrank_span_singleton hx
  have : y ∈ Submodule.span K {x} := by rw [this]; exact mem_top
  exact mem_span_singleton.1 this

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case add_comm
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ b✝ : Pre R X
⊢ liftFun R X f a✝ + liftFun R X f b✝ = liftFun R X f b✝ + liftFun R X f a✝

Tactic:
rw [add_comm]

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 : X → A
⊢ ∀ (x y : FreeAlgebra R X),
    Quot.liftOn (x * y) (liftFun R X f) ⋯ = Quot.liftOn x (liftFun R X f) ⋯ * Quot.liftOn y (liftFun R X f) ⋯

Tactic:
rintro ⟨⟩ ⟨⟩
    rfl

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 : X → A
⊢ ∀ (x y : FreeAlgebra R X),
    Quot.liftOn (x + y) (liftFun R X f) ⋯ = Quot.liftOn x (liftFun R X f) ⋯ + Quot.liftOn y (liftFun R X f) ⋯

Tactic:
rintro ⟨⟩ ⟨⟩
    rfl

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

Goal state before:
pp: case append_singleton
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
ps : List R[X]
p : R[X]
ihp : (∀ p ∈ ps, ∀ (k : ℕ), Commute (f (p.coeff k)) x) → eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod
hf : (∀ x_1 ∈ ps, ∀ (k : ℕ), Commute (f (x_1.coeff k)) x) ∧ ∀ (k : ℕ), Commute (f (p.coeff k)) x
⊢ eval₂ f x (ps ++ [p]).prod = (List.map (eval₂ f x) (ps ++ [p])).prod

Tactic:
simp [eval₂_mul_noncomm _ _ hf.2, ihp hf.1]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: E : Type u_4
inst✝⁵ : AddCommGroup E
F : Type u_5
inst✝⁴ : AddCommGroup F
K : Type u_7
L : Type u_8
inst✝³ : DivisionRing K
inst✝² : DivisionRing L
σ : K →+* L
inst✝¹ : Module K E
inst✝ : Module L F
f : E →ₛₗ.[σ] F
x : E
y : F
hx : x ∉ f.domain
⊢ ↑(f.supSpanSingleton x y hx) ⟨x, ⋯⟩ = y

Tactic:
simpa using supSpanSingleton_apply_smul_self f y hx 1

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

Goal state before:
pp: R : Type u
a : R
inst✝ : CommSemiring R
p q : R[X]
H : q.IsRoot a
⊢ eval a (p * q) = 0

Tactic:
eval_mul,

Goal state after:
R : Type u
a : R
inst✝ : CommSemiring R
p q : R[X]
H : q.IsRoot a
⊢ eval a p * eval a q = 0
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
a : R
inst✝ : CommSemiring R
p q : R[X]
H : p.IsRoot a
⊢ eval a (p * q) = 0

Tactic:
eval_mul,

Goal state after:
R : Type u
a : R
inst✝ : CommSemiring R
p q : R[X]
H : p.IsRoot a
⊢ eval a p * eval a q = 0
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
a : R
inst✝¹ : CommSemiring R
p q : R[X]
inst✝ : NoZeroDivisors R
⊢ eval a (p * q) = 0 ↔ eval a p = 0 ∨ eval a q = 0

Tactic:
eval_mul,

Goal state after:
R : Type u
a : R
inst✝¹ : CommSemiring R
p q : R[X]
inst✝ : NoZeroDivisors R
⊢ eval a p * eval a q = 0 ↔ eval a p = 0 ∨ eval a q = 0
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mk
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
fst✝ : E
snd✝ : F
⊢ (fst✝, snd✝) ∈ f.graph ↔ ∃ y, ↑y = (fst✝, snd✝).1 ∧ ↑f y = (fst✝, snd✝).2

Tactic:
simp_rw [mem_graph_iff', Prod.mk_inj]

Goal state after:
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
⊢ ↑x = 0 ↔ 0 ∣ x

Tactic:
by rw [zero_dvd_iff]; exact ⟨H x, by rintro rfl; simp⟩

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mpr.mk
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
hx' : (fst✝, snd✝) ∈ f.graph
h : (LinearMap.id.prodMap (-LinearMap.id)) (fst✝, snd✝) = (x_fst, x_snd)
⊢ (x_fst, x_snd) ∈ (-f).graph

Tactic:
simp only [LinearMap.prodMap_apply, LinearMap.id_coe, id, LinearMap.neg_apply,
    Prod.mk_inj] at h

Goal state after:
case mpr.mk
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
hx' : (fst✝, snd✝) ∈ f.graph
h : fst✝ = x_fst ∧ -snd✝ = x_snd
⊢ (x_fst, x_snd) ∈ (-f).graph
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Preorder β
f : α → β
s : Set α
a : α
h : IsMinOn f s a
⊢ f a ∈ lowerBounds (f '' s)

Tactic:
simpa [mem_lowerBounds] using! h

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
p : R[X]
i : ℕ
⊢ i ∈ (r • p).support → i ∈ p.support

Tactic:
hi

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
p : R[X]
i : ℕ
hi : i ∈ (r • p).support
⊢ i ∈ p.support
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
ι : Type u_1
l : List ι
f : ι → R[X]
n : ℕ
⊢ (List.map f l).sum.coeff n = (List.map (fun a ↦ (f a).coeff n) l).sum

Tactic:
coeff_list_sum,

Goal state after:
R : Type u
inst✝ : Semiring R
ι : Type u_1
l : List ι
f : ι → R[X]
n : ℕ
⊢ (List.map (⇑(lcoeff R n)) (List.map f l)).sum = (List.map (fun a ↦ (f a).coeff n) l).sum
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : p.degree ≤ 0
⊢ (C (p.coeff 0 + a)).natDegree = (C (p.coeff 0)).natDegree

Tactic:
natDegree_C,

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : p.degree ≤ 0
⊢ 0 = (C (p.coeff 0)).natDegree
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
h✝ : ¬p.natDegree = q.natDegree
h : p.natDegree < q.natDegree
⊢ q.natDegree < p.natDegree

Tactic:
rwa [natDegree_add_eq_right_of_natDegree_lt h] at 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
⊢ (p + q).leadingCoeff = p.leadingCoeff

Tactic:
rw [add_comm]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.degree < p.degree
⊢ (q + p).leadingCoeff = p.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p ^ n).natDegree ≤ n * p.natDegree

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih => grw [pow_succ, Nat.succ_mul, natDegree_mul_le, ih]

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

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

Tactic:
← Nat.cast_inj (R := WithBot ℕ),

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p ≠ 0
hq : q ≠ 0
⊢ ↑(p * q).natDegree = ↑(p.natDegree + q.natDegree)
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 1
n✝ n m : ℕ
⊢ p.coeff m.succ.succ = (C (p.coeff 1) * X + C (p.coeff 0)).coeff m.succ.succ

Tactic:
by
        have : degree p < m.succ.succ := lt_of_le_of_lt h Nat.one_lt_ofNat
        simp [coeff_eq_zero_of_degree_lt this]

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

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

Tactic:
by
    rw [← coeff_one_zero, ← hgf]
    simp

Goal state after:
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
⊢ (X ^ n + C a).degree = ↑n

Tactic:
by
  have : degree (C a) < degree ((X : R[X]) ^ n) := degree_C_le.trans_lt <| by
    rwa [degree_X_pow, Nat.cast_pos]
  rw [degree_add_eq_left_of_degree_lt this, degree_X_pow]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ (C (p.coeff b)).natDegree + (q ^ b).natDegree < p.natDegree * q.natDegree

Tactic:
natDegree_C,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ 0 + (q ^ b).natDegree < p.natDegree * q.natDegree
Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : CommSemiring A'
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p q : R[X]
x : A
x✝¹ x✝ : ↥R[x]
p' : R[X]
hp : (aeval x).toRingHom p' ∈ R[x]
q' : R[X]
hq : (aeval x).toRingHom q' ∈ R[x]
⊢ ⟨(aeval x).toRingHom p', hp⟩ * ⟨(aeval x).toRingHom q', hq⟩ =
    ⟨(aeval x).toRingHom q', hq⟩ * ⟨(aeval x).toRingHom p', hp⟩

Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MulMemClass.mk_mul_mk, ← map_mul,
        mul_comm p' q']

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ (∑ i ∈ range (p.natDegree + 1), C (p.coeff i) * (C r * X) ^ i).coeff n = p.coeff n * r ^ n

Tactic:
(commute_X _).symm.mul_pow,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ (∑ x ∈ range (p.natDegree + 1), C (p.coeff x) * (C r ^ x * X ^ x)).coeff n = p.coeff n * r ^ n
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ ∑ x ∈ range (p.natDegree + 1), p.coeff x * (r ^ x * if n = x then 1 else 0) = p.coeff n * r ^ n

Tactic:
rw [Finset.sum_eq_single n _ fun h ↦ ?_, if_pos rfl, mul_one]

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

R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.coeff n * (r ^ n * if n = n then 1 else 0) = 0
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : Type u_4
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : AddCommMonoid β
inst✝² : Preorder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
⊢ f₁.sum h ≤ f₂.sum h

Tactic:
by
  rw [sum_of_support_subset _ Finset.subset_union_left _ hh₀,
    sum_of_support_subset _ Finset.subset_union_right _ hh₀]
  gcongr with i hi
  exact hh _ hi <| hf _

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f : ι → κ
h : Function.Injective f
f1 f2 : ι →₀ α
⊢ mapDomain f (f1 - f2) = mapDomain f f1 - mapDomain f f2

Tactic:
by
  ext y
  by_cases! hy : y ∉ Set.range f
  · simp [mapDomain_of_notMem_range _ _ hy]
  · obtain ⟨x, rfl⟩ := hy
    simp [mapDomain_apply h]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
a : R
⊢ p ∣ q.comp (X + C a) ↔ p.comp (X - C a) ∣ q

Tactic:
simpa using! dvd_comp_X_sub_C_iff p q (-a)

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

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

Tactic:
hi

Goal state after:
case h
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
i : ℕ
hi : i > P.natDegree
⊢ P.coeff i • Q = 0
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 * Q).coeff (l + m) = P.coeff l * Q.leadingCoeff

Tactic:
rw [coeff_mul]

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
⊢ ∑ x ∈ antidiagonal (l + m), P.coeff x.1 * Q.coeff x.2 = P.coeff l * Q.leadingCoeff
Module: Mathlib.Algebra.MvPolynomial.Basic

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

Tactic:
hi

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → ℕ
t : Finset σ
i : σ
hi : i ∈ t
⊢ 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.Eval

Goal state before:
pp: 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 : MvPolynomial σ R
⊢ k (eval₂ f g p) = eval₂ (k.comp f) (⇑k ∘ g) p

Tactic:
apply MvPolynomial.induction_on p <;>
    simp +contextual [eval₂_add, k.map_add, eval₂_mul, k.map_mul]

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

Goal state before:
pp: case e_a
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
C : σ →₀ ℕ
hc : C ∈ p.coeff.support
i : σ
⊢ i ∈ C.support → (fun n e ↦ g₁ n ^ e) i (C i) = (fun n e ↦ g₂ n ^ e) i (C i)

Tactic:
hi

Goal state after:
case e_a
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
C : σ →₀ ℕ
hc : C ∈ p.coeff.support
i : σ
hi : i ∈ C.support
⊢ (fun n e ↦ g₁ n ^ e) i (C i) = (fun n e ↦ g₂ n ^ e) i (C i)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case a
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ q.support \ p.support ⊆ (p + q).support

Tactic:
rw [add_comm]

Goal state after:
case a
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ q.support \ p.support ⊆ (q + p).support
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p ≠ 0 ↔ ∃ d, coeff d p ≠ 0

Tactic:
rw [Ne, eq_zero_iff]
  push Not
  rfl

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₁
n : σ
⊢ (map f) (X n) = X n

Tactic:
simp [X]

Goal state after:
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
s : τ →₀ ℕ
c : R
hs : ↑s.support ⊆ range f
⊢ (killCompl hf) ((monomial (Finsupp.mapDomain f (Finsupp.comapDomain f s ⋯))) c) =
    (monomial (Finsupp.comapDomain f s ⋯)) c

Tactic:
killCompl_monomial_mapDomain

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
hs : ↑s.support ⊆ range f
⊢ (monomial (Finsupp.comapDomain f s ⋯)) c = (monomial (Finsupp.comapDomain f s ⋯)) c