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

Goal state before:
pp: case a
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] C
g : B →ₐ[R] D
⊢ ⇑(map f g) '' {t | ∃ a b, a ⊗ₜ[R] b = t} ⊆ ↑((includeLeft.comp f).range ⊔ (includeRight.comp g).range)

Tactic:
rintro _ ⟨_, ⟨a, b, rfl⟩, rfl⟩

Goal state after:
case a
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] C
g : B →ₐ[R] D
a : A
b : B
⊢ (map f g) (a ⊗ₜ[R] b) ∈ ↑((includeLeft.comp f).range ⊔ (includeRight.comp g).range)
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
⊢ toNat (lift.{u_2, v} (Module.rank R M)) = toNat (Module.rank R M)

Tactic:
toNat_lift

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

Goal state before:
pp: case inr
R✝ : Type u_1
A : Type u_2
inst✝⁷ : NonUnitalRing R✝
inst✝⁶ : PartialOrder R✝
inst✝⁵ : StarRing R✝
inst✝⁴ : StarOrderedRing R✝
p q : R✝
R : Type u_3
inst✝³ : NonUnitalRing R
inst✝² : LinearOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
r : R
hr : 0 ≤ -r
⊢ star r = r

Tactic:
· simpa using hr.star_eq

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 v
inst✝ : Fintype ι
⊢ toNat #ι * toNat (lift.{v, v} (Module.rank R M)) = toNat #ι * toNat (Module.rank R M)

Tactic:
toNat_lift

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 v
inst✝ : Fintype ι
⊢ toNat #ι * toNat (Module.rank R M) = toNat #ι * toNat (Module.rank R M)
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : StrongRankCondition R
ι : Type v
inst✝ : Fintype ι
⊢ toNat (lift.{u, v} #ι) = toNat #ι

Tactic:
toNat_lift

Goal state after:
R : Type u
inst✝² : Semiring R
inst✝¹ : StrongRankCondition R
ι : Type v
inst✝ : Fintype ι
⊢ toNat #ι = toNat #ι
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 : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i ↦ ↑i) → s.card ≤ n
s : Set M
li : LinearIndependent R Subtype.val
⊢ ∀ (s_1 : Finset ↑s), s_1.card ≤ n

Tactic:
intro t

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i ↦ ↑i) → s.card ≤ n
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
⊢ t.card ≤ n
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: 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
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Free R M
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Fintype η
n : ℕ
hn : Module.rank R M = ↑n
⊢ M ≃ₗ[R] Fin n → R

Tactic:
haveI := nontrivial_of_invariantBasisNumber R
  have : Cardinal.lift.{u} (n : Cardinal.{v}) = Cardinal.lift.{v} (n : Cardinal.{u}) := by simp
  have hn := Cardinal.lift_inj.{v, u}.2 hn
  rw [this] at hn
  rw [← @rank_fin_fun R _ _ n] at hn
  haveI : Module.Free R (Fin n → R) := Module.Free.pi _ _
  exact Classical.choice (nonempty_linearEquiv_of_lift_rank_eq hn)

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
s : Submodule R M
lt : finrank R ↥s < finrank R ↥⊤
⊢ s < ⊤

Tactic:
exact lt_of_le_of_finrank_lt_finrank le_top lt

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
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
⊢ Set.finrank R (range b) ≤ Fintype.card ι

Tactic:
refine (finrank_span_le_card _).trans ?_

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
⊢ (range b).toFinset.card ≤ Fintype.card ι
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 (NonUnitalStarSubalgebra R A)
x : A
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
by
  simp only [← SetLike.mem_coe, coe_sInf, Set.mem_iInter₂]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case neg
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : V
hfv : f v ≠ 0
b₁ : Basis (↑(Basis.ofVectorSpaceIndex K ↥f.ker)) K ↥f.ker := ⋯
s : Set V := ⋯
hs : span K s = f.ker
n : Set V := ⋯
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := ⋯
i : ↑n := ⋯
hi : b i = v
j : ↑n
h : ¬i = j
⊢ _root_.id ↑j ∈ s

Tactic:
apply Or.resolve_left (Set.mem_insert_iff.mpr j.prop)

Goal state after:
case neg
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : V
hfv : f v ≠ 0
b₁ : Basis (↑(Basis.ofVectorSpaceIndex K ↥f.ker)) K ↥f.ker := ⋯
s : Set V := ⋯
hs : span K s = f.ker
n : Set V := ⋯
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := ⋯
i : ↑n := ⋯
hi : b i = v
j : ↑n
h : ¬i = j
⊢ ¬↑j = v
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : StrongRankCondition R
v : M
n : v ≠ 0
h : ∀ (w : M), ∃ c, c • v = w
this : Nontrivial R
b : Basis PUnit.{u + 1} R M
⊢ ↑(Fintype.card PUnit.{u + 1}) = 1

Tactic:
Fintype.card_punit,

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : StrongRankCondition R
v : M
n : v ≠ 0
h : ∀ (w : M), ∃ c, c • v = w
this : Nontrivial R
b : Basis PUnit.{u + 1} R M
⊢ ↑1 = 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
EQ : f = g
x y : ↥f.domain
h : ↑x = ↑y
⊢ ↑f x = ↑f y

Tactic:
by
        congr
        exact mod_cast h

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

Goal state before:
pp: case mp
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
h : c ≤ Module.rank K V
⊢ ∃ s, #↑s = c ∧ LinearIndepOn K id s

Tactic:
obtain ⟨κ, t'⟩ := Module.Free.exists_basis (R := K) (M := V)

Goal state after:
case mp
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
h : c ≤ Module.rank K V
κ : Type v
t' : Basis κ K V
⊢ ∃ s, #↑s = c ∧ LinearIndepOn K id s
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
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
hinj : Injective ⇑f
⊢ Surjective ⇑f

Tactic:
have h := rank_range_of_injective _ hinj
  rw [← finrank_eq_rank, ← finrank_eq_rank, Nat.cast_inj] at h
  exact range_eq_top.1 (eq_top_of_finrank_eq h)

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case w.refine_1
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
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
z₁ : E
hz₁ : z₁ ∈ f.domain ⊔ g.domain
z₂ : E
hz₂ : z₂ ∈ f.domain ⊔ g.domain
⊢ fg (⟨z₁, hz₁⟩ + ⟨z₂, hz₂⟩) = ↑f ⟨x ⟨z₁, hz₁⟩, ⋯⟩ + ↑f ⟨x ⟨z₂, hz₂⟩, ⋯⟩ + ↑g ⟨y ⟨z₁, hz₁⟩, ⋯⟩ + ↑g ⟨y ⟨z₂, hz₂⟩, ⋯⟩

Tactic:
← map_add,

Goal state after:
case w.refine_1
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
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
z₁ : E
hz₁ : z₁ ∈ f.domain ⊔ g.domain
z₂ : E
hz₂ : z₂ ∈ f.domain ⊔ g.domain
⊢ fg (⟨z₁, hz₁⟩ + ⟨z₂, hz₂⟩) = ↑f (⟨x ⟨z₁, hz₁⟩, ⋯⟩ + ⟨x ⟨z₂, hz₂⟩, ⋯⟩) + ↑g ⟨y ⟨z₁, hz₁⟩, ⋯⟩ + ↑g ⟨y ⟨z₂, hz₂⟩, ⋯⟩
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case h'
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
f g h : E →ₛₗ.[σ] F
x : E
y : x ∈ (f + g + h).domain
hxy : x ∈ (f + (g + h)).domain
⊢ ↑(f + g + h) ⟨x, y⟩ = ↑(f + (g + h)) ⟨x, hxy⟩

Tactic:
· simp only [add_apply, add_assoc]

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

Goal state before:
pp: case hf
R : Type u
S : Type v
a : R
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
h : Commute (f a) x
k : ℕ
⊢ Commute (f ((C a).coeff k)) x

Tactic:
by_cases hk : k = 0

Goal state after:
case pos
R : Type u
S : Type v
a : R
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
h : Commute (f a) x
k : ℕ
hk : k = 0
⊢ Commute (f ((C a).coeff k)) x

case neg
R : Type u
S : Type v
a : R
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
h : Commute (f a) x
k : ℕ
hk : ¬k = 0
⊢ Commute (f ((C a).coeff k)) x
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
n : ℕ
inst✝ : n.AtLeastTwo
a : R
⊢ eval a (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
by
  simp only [OfNat.ofNat, eval_natCast]

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

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

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

Tactic:
· exact h₀ ⟨hx.1, g₀⟩ (right_mem_Ioc.2 (g₀.trans_lt' hx.1)) g₀

Goal state after:
case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ioo a c
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

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

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

Tactic:
· exact h₀ ⟨hx.1, g₀⟩ (right_mem_Ioc.2 (g₀.trans_lt' hx.1)) g₀

Goal state after:
case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Ioc a c
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Algebra.Polynomial.Coeff

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

Tactic:
rcases p with ⟨⟩

Goal state after:
R : Type u
inst✝ : Semiring R
q : R[X]
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝ } + q).coeff n = { toFinsupp := toFinsupp✝ }.coeff n + q.coeff n
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
by_cases hp2 : p ^ i = 0

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

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

Goal state before:
pp: R : Type u
a b : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C b).degree < (C a * X).degree

Tactic:
simpa only [degree_C_mul_X ha] using degree_C_lt

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Tactic:
by
  by_cases hp : p = 0
  · simp only [hp, zero_mul, leadingCoeff_zero]
  · by_cases hq : q = 0
    · simp only [hq, mul_zero, leadingCoeff_zero]
    · rw [leadingCoeff_mul']
      exact mul_ne_zero (mt leadingCoeff_eq_zero.1 hp) (mt leadingCoeff_eq_zero.1 hq)

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

Goal state before:
pp: case ha
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
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ ¬leadingCoeff D p = 0

Tactic:
leadingCoeff_eq_zero hD

Goal state after:
case ha
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
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ ¬p = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case hb
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
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ ¬leadingCoeff D q = 0

Tactic:
leadingCoeff_eq_zero hD

Goal state after:
case hb
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
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ ¬q = 0
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: case mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : (x + y) i = (single a n) i
⊢ (single a (x a)) i = x i ∧ (single a (y a)) i = y i

Tactic:
single_apply,

Goal state after:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : (x + y) i = if a = i then n else 0
⊢ (if a = i then x a else 0) = x i ∧ (if a = i then y a else 0) = y i
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
f : F
x : A
p : R[X]
⊢ ∀ (a : R), (aeval (f x)) (C a) = f ((aeval x) (C a))

Tactic:
simp [AlgHomClass.commutes]

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

Goal state before:
pp: R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
f : F
x : A
p : R[X]
⊢ ∀ (n : ℕ) (a : R),
    (aeval (f x)) (C a * X ^ n) = f ((aeval x) (C a * X ^ n)) →
      (aeval (f x)) (C a * X ^ (n + 1)) = f ((aeval x) (C a * X ^ (n + 1)))

Tactic:
simp [AlgHomClass.commutes]

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

Goal state before:
pp: R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
f : F
x : A
p✝ p q : R[X]
hp : (aeval (f x)) p = f ((aeval x) p)
hq : (aeval (f x)) q = f ((aeval x) q)
⊢ f ((aeval x) p) + f ((aeval x) q) = f ((aeval x) (p + q))

Tactic:
← map_add,

Goal state after:
R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
f : F
x : A
p✝ p q : R[X]
hp : (aeval (f x)) p = f ((aeval x) p)
hq : (aeval (f x)) q = f ((aeval x) q)
⊢ f ((aeval x) p + (aeval x) q) = f ((aeval x) (p + q))
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝ : (i : ι) → PartialOrder (β i)
r : ι → ι → Prop
hwf : WellFounded r
x y : (i : ι) → β i
hlt : x < y
⊢ Pi.Lex r (fun {i} x1 x2 ↦ x1 < x2) x y

Tactic:
by
  simp_rw [Pi.Lex, le_antisymm_iff]
  exact lex_lt_of_lt_of_preorder hwf hlt

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

Goal state before:
pp: case add
R : Type u
A : Type z
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
q : Submodule R M
m : M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hm : m ∈ q
a : A
hq : q ≤ Submodule.comap ((Algebra.lsmul R R M) a) q
f₁ f₂ : R[X]
h₁ : (aeval a) f₁ • m ∈ q
h₂ : (aeval a) f₂ • m ∈ q
⊢ (aeval a) (f₁ + f₂) • m ∈ q

Tactic:
simp_rw [map_add, add_smul]

Goal state after:
case add
R : Type u
A : Type z
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
q : Submodule R M
m : M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hm : m ∈ q
a : A
hq : q ≤ Submodule.comap ((Algebra.lsmul R R M) a) q
f₁ f₂ : R[X]
h₁ : (aeval a) f₁ • m ∈ q
h₂ : (aeval a) f₂ • m ∈ q
⊢ (aeval a) f₁ • m + (aeval a) f₂ • m ∈ q
Module: Mathlib.Algebra.MvPolynomial.Basic

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

Tactic:
rw [X_pow_eq_monomial, support_monomial, if_neg (one_ne_zero' R)]

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

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

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:
· exact support_sdiff_support_subset_support_add p q

Goal state after:
case a
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ q.support \ p.support ⊆ (p + q).support
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 : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p) →
      k (eval₂ f g q) = eval₂ k (⇑k ∘ g) ((map f) q) → k (eval₂ f g (p + q)) = eval₂ k (⇑k ∘ g) ((map f) (p + q))

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

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

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial (↥s₁) R
s₂ : Finset σ
q₂ : MvPolynomial (↥s₂) R
⊢ ∃ s q₁_1 q₂_1,
    (rename Subtype.val) q₁ = (rename Subtype.val) q₁_1 ∧ (rename Subtype.val) q₂ = (rename Subtype.val) q₂_1

Tactic:
classical
    use s₁ ∪ s₂
    use rename (fun x ↦ ⟨x, Finset.subset_union_left x.2⟩) q₁
    use rename (fun x ↦ ⟨x, Finset.subset_union_right x.2⟩) q₂
    constructor <;> simp [Function.comp_def]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ (degrees 0).toFinset = ∅

Tactic:
degrees_zero,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ Multiset.toFinset 0 = ∅
Module: Mathlib.Algebra.MvPolynomial.Degrees

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

Tactic:
hk

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

Goal state before:
pp: case a.add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
p q : MvPolynomial σ R
hp : (aeval f) p ∈ Algebra.adjoin R (range f)
hq : (aeval f) q ∈ Algebra.adjoin R (range f)
⊢ (aeval f) (p + q) ∈ Algebra.adjoin R (range f)

Tactic:
rw [map_add]; exact Subalgebra.add_mem _ hp hq

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

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
⊢ (eval₂Hom f g) (∑ v ∈ p.support, (monomial v) (coeff v p)) = f (constantCoeff p)

Tactic:
simp only [map_sum, eval₂Hom_monomial]

Goal state after:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
⊢ (∑ x ∈ p.support, f (coeff x p) * x.prod fun i k ↦ g i ^ k) = f (constantCoeff p)
Module: Mathlib.Algebra.MvPolynomial.Degrees

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

Tactic:
hk

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