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

Goal state before:
pp: R : Type u_1
M : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} ≤ ((mk R S M) 1).range

Tactic:
Submodule.span_le

Goal state after:
R : Type u_1
M : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ {t | ∃ m n, m ⊗ₜ[R] n = t} ⊆ ↑((mk R S M) 1).range
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
S : Type u_3
T : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
⊢ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} ≤ ((mk R S T).flip 1).range

Tactic:
Submodule.span_le

Goal state after:
R : Type u_1
S : Type u_3
T : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
⊢ {t | ∃ m n, m ⊗ₜ[R] n = t} ⊆ ↑((mk R S T).flip 1).range
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
⊢ ∀ (a₁ a₂ : R) (b₁ b₂ : A),
    (_root_.TensorProduct.lid R A) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      (_root_.TensorProduct.lid R A) (a₁ ⊗ₜ[R] b₁) * (_root_.TensorProduct.lid R A) (a₂ ⊗ₜ[R] b₂)

Tactic:
by
    simp only [mul_smul, lid_tmul, Algebra.smul_mul_assoc, Algebra.mul_smul_comm]
    simp_rw [← mul_smul, mul_comm]
    simp

Goal state after:
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:
by simp_all [add_tmul]

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

Goal state before:
pp: case mem
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r✝ : R
a : A
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
r : R
hr : r ∈ range fun s ↦ star s * s
⊢ r • a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)

Tactic:
induction ha using AddSubmonoid.closure_induction with

Goal state after:
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 b : R
hab : a < b
c : R
hc : IsRegular c
⊢ star c * a * c ≠ star c * b * c

Tactic:
hc.right.ne_iff,

Goal state after:
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : a < b
c : R
hc : IsRegular c
⊢ star c * a ≠ star c * b
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
⊢ ?m.52

Tactic:
by simpa [← mul_assoc] using star_right_conjugate_nonneg h v

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

Goal state before:
pp: 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
inst✝ : Module.Free R A
⊢ centralizer R ↑(Algebra.TensorProduct.map (Algebra.ofId R A) (AlgHom.id R B)).range =
    (Algebra.TensorProduct.map (AlgHom.id R A) (center R B).val).range

Tactic:
rw [← centralizer_range_includeRight_eq_center_tensorProduct]
  simp [Algebra.TensorProduct.map_range]

Goal state after:
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
n : ℕ
hn : ↑n ≤ Module.rank R M
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
rcases hn.eq_or_lt with h | h
  · obtain ⟨⟨s, hs⟩, hs'⟩ := exists_eq_ciSup_of_not_isSuccLimit
      Cardinal.bddAbove_of_small (h.trans (Module.rank_def R M) ▸ not_isSuccLimit_natCast n)
    rw [← Module.rank_def, ← h] at hs'
    have : Finite s := lt_aleph0_iff_finite.mp (hs' ▸ natCast_lt_aleph0)
    cases nonempty_fintype s
    refine ⟨s.toFinset, by simpa using hs', by simpa⟩
  · obtain ⟨s, hs, hs'⟩ := exists_set_linearIndependent_of_lt_rank h
    have : Finite s := lt_aleph0_iff_finite.mp (hs ▸ natCast_lt_aleph0)
    cases nonempty_fintype s
    exact ⟨s.toFinset, by simpa using hs, by simpa⟩

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)
v : V
hv : v ∈ W
j : n
⊢ ((bW.sumQuot bQ).repr v) (Sum.inr j) = 0

Tactic:
suffices W.mkQ v = 0 by simp [sumQuot_repr_inr, this]

Goal state after:
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)
v : V
hv : v ∈ W
j : n
⊢ W.mkQ v = 0
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: 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
⊢ ∀ (c₁ c₂ : R), c₁ • x = c₂ • x → σ c₁ • y = σ c₂ • y

Tactic:
intro c₁

Goal state after:
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
c₁ : R
⊢ ∀ (c₂ : R), c₁ • x = c₂ • x → σ c₁ • y = σ c₂ • y
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: 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
⊢ ∀ (c₁ c₂ : R), c₁ • x = c₂ • x → σ c₁ • y = σ c₂ • y

Tactic:
intro c₁ c₂ h
      rw [← sub_eq_zero, ← sub_smul] at h ⊢
      rw [← RingHom.map_sub]
      exact H _ h

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

Goal state before:
pp: case mpr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this : Nontrivial K
⊢ (∃ s, #↑s = c ∧ LinearIndepOn K id s) → c ≤ Module.rank K V

Tactic:
rintro ⟨s, rfl, si⟩

Goal state after:
case mpr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this : Nontrivial K
s : Set V
si : LinearIndepOn K id s
⊢ #↑s ≤ Module.rank K V
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case mpr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
n : ℕ
⊢ (∃ s, s.card = n ∧ LinearIndependent K Subtype.val) → ∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K id s

Tactic:
rintro ⟨s, rfl, si⟩

Goal state after:
case mpr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
s : Finset V
si : LinearIndependent K Subtype.val
⊢ ∃ s_1, (∃ t, ↑t = s_1 ∧ t.card = s.card) ∧ LinearIndepOn K id s_1
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case insert
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
⊢ (f i).ker ⊔ (s.noncommProd f ⋯).ker = ⨆ i_1 ∈ insert i s, (f i_1).ker

Tactic:
Finset.mem_insert_coe,

Goal state after:
case insert
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
⊢ (f i).ker ⊔ (s.noncommProd f ⋯).ker = ⨆ i_1 ∈ insert i ↑s, (f i_1).ker
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
⊢ f.ker = ⊥ → IsUnit f

Tactic:
· intro h_inj
    rw [ker_eq_bot] at h_inj
    exact ⟨⟨f, (LinearEquiv.ofInjectiveEndo f h_inj).symm.toLinearMap,
      LinearEquiv.ofInjectiveEndo_right_inv f h_inj, LinearEquiv.ofInjectiveEndo_left_inv f h_inj⟩,
      rfl⟩

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mp
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
y : ↥(-f).domain
hy : ↑y = (x_fst, x_snd).1
h : ↑(-f) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph

Tactic:
rw [LinearPMap.neg_apply] at h

Goal state after:
case mp
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
y : ↥(-f).domain
hy : ↑y = (x_fst, x_snd).1
h : -↑f y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Icc b a)
x : α
hx : x ∈ Iic a
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
exact h₁ (left_mem_Icc.2 (g₀.le.trans hx)) ⟨g₀.le, hx⟩ g₀.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✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f : R[A]
fs : List R[A]
⊢ (f :: fs).prod.coeff.support.sup degb ≤ (List.map (fun f ↦ f.coeff.support.sup degb) (f :: fs)).sum

Tactic:
List.prod_cons,

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f : R[A]
fs : List R[A]
⊢ (f * fs.prod).coeff.support.sup degb ≤ (List.map (fun f ↦ f.coeff.support.sup degb) (f :: fs)).sum
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case h
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
a✝ : List R[A]
⊢ (Multiset.prod (Quot.mk (⇑(List.isSetoid R[A])) a✝)).coeff.support.sup degb ≤
    (Multiset.map (fun f ↦ f.coeff.support.sup degb) (Quot.mk (⇑(List.isSetoid R[A])) a✝)).sum

Tactic:
rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.sum_coe, Multiset.prod_coe]

Goal state after:
case h
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
a✝ : List R[A]
⊢ a✝.prod.coeff.support.sup degb ≤ (List.map (fun f ↦ f.coeff.support.sup degb) a✝).sum
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
if_neg (Nat.succ_ne_zero _),

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 0
n : ℕ
⊢ p.coeff (n + 1) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Support

Goal state before:
pp: case neg
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < ↑n
hp : ¬p = 0
⊢ ∑ i, f (↑i) (p.coeff ↑i) = ∑ a ∈ range n, f a (p.coeff a)

Tactic:
Fin.sum_univ_eq_sum_range fun i => f i (p.coeff i)

Goal state after:
case neg
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < ↑n
hp : ¬p = 0
⊢ ∑ i ∈ range n, f i (p.coeff i) = ∑ a ∈ range n, f a (p.coeff a)
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
a b : WithBot ℕ
hp : p.degree ≤ a
hq : q.degree ≤ b
⊢ (p * q).degree ≤ a + b

Tactic:
degree_mul_le,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
a b : WithBot ℕ
hp : p.degree ≤ a
hq : q.degree ≤ b
⊢ p.degree + q.degree ≤ a + b
Module: Mathlib.Algebra.Polynomial.Degree.Defs

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

Tactic:
degree_mul_le,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p ^ n).degree + p.degree ≤ n • p.degree + p.degree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ (p * q).leadingCoeff = q.leadingCoeff

Tactic:
rw [leadingCoeff_mul', hp.leadingCoeff, one_mul]
    rwa [hp.leadingCoeff, one_mul, Ne, leadingCoeff_eq_zero]

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι✝ : Type y
a b : R✝
m n✝ : ℕ
inst✝³ : Semiring R✝
p✝ q r : R✝[X]
inst✝² : Semiring S
f : R✝ →+* S
ι : Type ?u.38
inst✝¹ : Finite ι
R : ι → Type u_1
inst✝ : (i : ι) → Semiring (R i)
p : (i : ι) → (R i)[X]
n : ℕ
hn : n ∈ Function.support fun n i ↦ (p i).coeff n
⊢ n ∈ ⋃ i, ↑(p i).support

Tactic:
simp only [Set.mem_iUnion, Finset.mem_coe, mem_support_iff, Function.mem_support] at hn ⊢
          contrapose! hn; exact funext hn

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

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

Tactic:
rw [Monic, hq.leadingCoeff_mul_eq_left hD hadd]

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
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
hq : Monic D q
⊢ leadingCoeff D p = 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
⊢ ↑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))

Tactic:
Nat.choose_self,

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 * (↑1 * 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: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : p.Monic
hfp : map f p = 0
x : R
⊢ f x = f x * f p.leadingCoeff

Tactic:
simp only [mul_one, hp.leadingCoeff, f.map_one]

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

Goal state before:
pp: case neg
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : 0 < p.natDegree
H : ¬map f p = 0
⊢ (map f p).natDegree < p.natDegree

Tactic:
exact natDegree_map_lt hp H

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝² : Preorder ι
inst✝¹ : DecidableEq ι
inst✝ : LT α
f : ι → α
i j : ι
h₁ : i ≤ j
h₂ : f j < f i
⊢ (fun {i} x1 x2 ↦ x1 < x2) (toLex (f ∘ ⇑(Equiv.swap i j)) i) (toLex f i)

Tactic:
simpa only [Pi.toLex_apply, Function.comp_apply, Equiv.swap_apply_left] using h₂

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

Goal state before:
pp: 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 : ℕ := ⋯
⊢ ∀ b ∈ antidiagonal (l + m), b ≠ (l, m) → P.coeff b.1 * Q.coeff b.2 = 0

Tactic:
simp only [Finset.mem_antidiagonal, ne_eq, Prod.forall, Prod.mk.injEq, not_and]

Goal state after:
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
⊢ ∀ (a b : ℕ), a + b = l + m → (a = l → ¬b = m) → P.coeff a * Q.coeff b = 0
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case inr.inl
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
m : ℕ := Q.natDegree
i j : ℕ
IH : ∀ m > i, P.coeff m • Q = 0
hl : (P.coeff i • Q).natDegree = Q.natDegree
hij : i + j = i + m
H : i = i → ¬j = m
⊢ P.coeff i * Q.coeff j = 0

pp: case inr.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
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
hi : l < i
⊢ P.coeff i * Q.coeff j = 0

Tactic:
· lia

Goal state after:
case inr.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
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
hi : l < i
⊢ P.coeff i * Q.coeff j = 0
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 : σ → S₁
p : MvPolynomial σ R
n : σ
ih : ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e
s : σ →₀ ℕ
a : R
⊢ eval₂ f g (p * X n * (monomial s) a) = eval₂ f g (p * (monomial (Finsupp.single n 1 + s)) a)

Tactic:
rw [monomial_single_add, pow_one, mul_assoc]

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

Goal state before:
pp: R : Type u
σ : Type u_1
n : σ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ((monomial (Finsupp.single n 1)) 1).support = {Finsupp.single n 1}

Tactic:
support_monomial,

Goal state after:
R : Type u
σ : Type u_1
n : σ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ (if 1 = 0 then ∅ else {Finsupp.single n 1}) = {Finsupp.single n 1}
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
n : ℕ
⊢ ((monomial (Finsupp.single s n)) 1).support = {Finsupp.single s n}

Tactic:
support_monomial,

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
n : ℕ
⊢ (if 1 = 0 then ∅ else {Finsupp.single s n}) = {Finsupp.single s n}
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 + q)) = eval₂ C (⇑(map f) ∘ g) ((map f) (p + q))

Tactic:
rw [eval₂_add, (map f).map_add, hp, hq, (map f).map_add, eval₂_add]

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

Goal state before:
pp: case pos
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝¹ : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
inst✝ : Decidable (↑s.support ⊆ range f)
h : ↑s.support ⊆ range f
⊢ (killCompl hf) ((monomial s) c) = (monomial (Finsupp.comapDomain f s ⋯)) c

pp: case neg
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝¹ : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
inst✝ : Decidable (↑s.support ⊆ range f)
h : ¬↑s.support ⊆ range f
⊢ (killCompl hf) ((monomial s) c) = 0

Tactic:
· exact killCompl_monomial_eq_monomial_comapDomain_of_subset hf c h

Goal state after:
case neg
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝¹ : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
inst✝ : Decidable (↑s.support ⊆ range f)
h : ¬↑s.support ⊆ range f
⊢ (killCompl hf) ((monomial s) c) = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ ((monomial s) a).degrees = toMultiset s

Tactic:
by
  classical
    exact (supDegree_single s a).trans (if_neg ha)

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

Goal state before:
pp: S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x : MvPolynomial R ℤ
n : ℤ
⊢ eval₂ c (⇑f ∘ X) (C n) = f (C n)

Tactic:
rw [hom_C f, eval₂_C]
      exact eq_intCast c n

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
a b : MvPolynomial σ R
⊢ max a.totalDegree (-b).totalDegree = max a.totalDegree b.totalDegree

Tactic:
rw [totalDegree_neg]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Fin

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
⊢ (cons i σ).sum f = f 0 i + σ.sum (Fin.tail f)

Tactic:
rw [sum_fintype _ _ (fun _ => by apply h), sum_fintype _ _ (fun _ => by apply h)]

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
⊢ ∑ i_1, f i_1 ((cons i σ) i_1) = f 0 i + ∑ i, Fin.tail f i (σ i)