mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
x : M
hx : ∀ (a : R), a ≠ 0 → a • x ≠ 0
⊢ 1 ≤ Module.rank R M

Tactic:
have : LinearIndependent R (fun _ : Unit ↦ x) :=
      linearIndependent_iff.mpr (fun l hl ↦ Finsupp.unique_ext <| not_not.mp fun H ↦
        hx _ H ((Finsupp.linearCombination_unique _ _ _).symm.trans hl))

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
x : M
hx : ∀ (a : R), a ≠ 0 → a • x ≠ 0
this : LinearIndependent R fun x_1 ↦ x
⊢ 1 ≤ Module.rank R M
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: F : Type u_2
E : Type u_3
inst✝⁶ : CommRing F
inst✝⁵ : IsDomain F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : IsTorsionFree F E
inst✝ : Nontrivial E
⊢ Module.rank F ↥1 = 1

Tactic:
one_eq_span,

Goal state after:
F : Type u_2
E : Type u_3
inst✝⁶ : CommRing F
inst✝⁵ : IsDomain F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : IsTorsionFree F E
inst✝ : Nontrivial E
⊢ Module.rank F ↥(F ∙ 1) = 1
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)
w : ↥W
i : m
⊢ ((bW.sumQuot bQ).repr ↑w) (Sum.inl i) = (bW.repr w) i

Tactic:
refine Eq.symm <| (bW.repr_apply_eq
      (fun w i => (sumQuot bW bQ).repr (W.subtype w) (Sum.inl i)) ?_ ?_ ?_ w i) <;>
  aesop (add simp Finsupp.single_apply)

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
inst✝ : Free R M
h : ∀ (s : Finset M) (a : Basis (↑↑s) R M), False
s : Set M
b : Basis (↑s) R M
hs : s.Finite
⊢ Basis (↑↑hs.toFinset) R M

Tactic:
convert! b
        simp

Goal state after:
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
S : Submodule K V
h : finrank K ↥S = finrank K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this✝ : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)
b : Basis (↑(this✝.extend ⋯)) K V := Basis.extend this✝
b_eq : b = Basis.extend this✝
i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
this : Subtype.val '' Basis.ofVectorSpaceIndex K ↥S = this✝.extend ⋯
⊢ S = ⊤

Tactic:
← b.span_eq,

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this✝ : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)
b : Basis (↑(this✝.extend ⋯)) K V := Basis.extend this✝
b_eq : b = Basis.extend this✝
i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
this : Subtype.val '' Basis.ofVectorSpaceIndex K ↥S = this✝.extend ⋯
⊢ S = span K (Set.range ⇑b)
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₁⟩, ⋯⟩ + ⟨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₁⟩, ⋯⟩ + ⟨y ⟨z₂, hz₂⟩, ⋯⟩)
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ ∀ (a : FreeAlgebra R X), 0 * a = 0

Tactic:
rintro ⟨⟩
    exact Quot.sound Rel.zero_mul

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case add_compat_left
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✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f a✝¹ + liftFun R X f c✝ = liftFun R X f (b✝ + c✝)

pp: case add_compat_right
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✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ + a✝¹) = liftFun R X f (c✝ + b✝)

pp: case mul_compat_left
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✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)

pp: case mul_compat_right
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✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)

Tactic:
simp only [*]

Goal state after:
case add_compat_left
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✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f b✝ + liftFun R X f c✝ = liftFun R X f (b✝ + c✝)

case add_compat_right
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✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ + a✝¹) = liftFun R X f (c✝ + b✝)

case mul_compat_left
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✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)

case mul_compat_right
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✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case add_compat_right
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✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f c✝ + liftFun R X f a✝¹ = liftFun R X f (c✝ + b✝)

pp: case mul_compat_left
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✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)

pp: case mul_compat_right
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✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)

Tactic:
simp only [*]

Goal state after:
case add_compat_right
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✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f c✝ + liftFun R X f b✝ = liftFun R X f (c✝ + b✝)

case mul_compat_left
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✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)

case mul_compat_right
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✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x (p * X) = eval₂ f x p * x

Tactic:
eval₂_mul_X

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x p * x = eval₂ f x p * x
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mul_compat_left
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✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f a✝¹ * liftFun R X f c✝ = liftFun R X f (b✝ * c✝)

pp: case mul_compat_right
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✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)

Tactic:
simp only [*]

Goal state after:
case mul_compat_left
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✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f b✝ * liftFun R X f c✝ = liftFun R X f (b✝ * c✝)

case mul_compat_right
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✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mul_compat_right
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✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f c✝ * liftFun R X f a✝¹ = liftFun R X f (c✝ * b✝)

Tactic:
simp only [*]

Goal state after:
case mul_compat_right
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✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f c✝ * liftFun R X f b✝ = liftFun R X f (c✝ * b✝)
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk.ofScalar
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
x : R
⊢ (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.ofScalar x)) = F (Quot.mk (Rel R X) (Pre.ofScalar x))

Tactic:
change algebraMap _ _ x = F (algebraMap _ _ x)

Goal state after:
case mk.ofScalar
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
x : R
⊢ (algebraMap R A) x = F ((algebraMap R (FreeAlgebra R X)) x)
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
x : R
⊢ eval x (C a * p) = a * eval x p

Tactic:
induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [mul_add, eval_add, ph, qh]
  | monomial n b => simp only [mul_assoc, C_mul_monomial, eval_monomial]

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case neg
n : ℕ
n1 : ¬n = 1
⊢ 0 < n.minFac

Tactic:
exact (minFac_prime n1).pos

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: 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
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ ↑g.toLinearPMap x = valFromGraph hg ⋯

Tactic:
change (if hg : _ then g.toLinearPMapAux hg else 0) x = _

Goal state after:
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
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ (if hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0 then g.toLinearPMapAux hg else 0) x = valFromGraph hg ⋯
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
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g.toLinearPMap.graph
⊢ (x_fst, x_snd) ∈ g

Tactic:
rw [LinearPMap.mem_graph_iff] at hx
    rcases hx with ⟨y, hx1, hx2⟩
    convert! g.mem_graph_toLinearPMap hg y using 1
    exact Prod.ext hx1.symm hx2.symm

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
f : R[X]
n✝ : ℕ
⊢ (C a * f).coeff n✝ = (a • f).coeff n✝

Tactic:
rw [coeff_C_mul, coeff_smul, smul_eq_mul]

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

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

Tactic:
by
  rw [coeff_mul, Finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]
  · rintro ⟨i, j⟩ h1 h2
    rw [coeff_X_pow, if_neg, mul_zero]
    grind [mem_antidiagonal]
  · grind [mem_antidiagonal]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
a : R
ha : a = 0
this : C a = 0
⊢ (C a).natDegree = 0

Tactic:
rw [natDegree, degree_eq_bot.2 this, WithBot.unbotD_bot]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
h✝ : ¬a = 0
⊢ (insert n p.support).max ≤ max p.degree ↑n

Tactic:
· rw [max_insert, max_comm]
    exact le_rfl

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ (C a * X ^ n).leadingCoeff = a

Tactic:
by
  rw [C_mul_X_pow_eq_monomial, leadingCoeff_monomial]

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

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

Tactic:
rcases eq_or_ne q 0 with (rfl | H)
  · simp
  · rw [leadingCoeff_mul', hp.leadingCoeff, one_mul]
    rwa [hp.leadingCoeff, one_mul, Ne, leadingCoeff_eq_zero]

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ (C a * p).natDegree = p.natDegree

Tactic:
by
  simp [natDegree, degree_C_mul_of_isUnit ha]

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

Goal state before:
pp: R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X ^ 2 + C b * X + C c).leadingCoeff = a

Tactic:
by
  rw [add_assoc, add_comm, leadingCoeff_add_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha,
    leadingCoeff_C_mul_X_pow]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff ≠ q.leadingCoeff
⊢ p.degree = (-q).degree

Tactic:
q.degree_neg

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff ≠ q.leadingCoeff
⊢ p.degree = q.degree
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
b : ℕ
x✝ : b ∈ p.support
hb : b ≠ 0
⊢ (fun e a ↦ a * 0 ^ e) b (p.coeff b) = 0

Tactic:
simp [zero_pow hb]

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
f : α →₀ ℕ
p : (α →₀ ℕ) × (α →₀ ℕ)
⊢ p ∈ f.antidiagonal'.support ↔ p.1 + p.2 = f

Tactic:
rcases p with ⟨p₁, p₂⟩
    simp [antidiagonal', ← and_assoc, Multiset.toFinsupp_eq_iff,
    ← Multiset.toFinsupp_eq_iff (f := f)]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedAddMonoid α
f : ι → κ
⊢ Monotone (mapDomain f)

Tactic:
exact fun g₁ g₂ h ↦ sum_le_sum_index h (fun _ _ ↦ single_mono) (by simp)

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 + (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 + q)) = f ((aeval x) (p + q))
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
this : ∀ (i : ℕ), P.coeff i • Q = 0
⊢ Q = 0

Tactic:
rw [← leadingCoeff_eq_zero]
    apply h
    simpa [ext_iff, mul_comm Q.leadingCoeff] using fun i ↦ congr_arg (·.coeff Q.natDegree) (this i)

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

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

Tactic:
by
  rw [monomial_eq, C_1, one_mul, Finsupp.prod, Finset.prod_subset (support_indicator_subset _ _)]
  · exact Finset.prod_congr rfl (fun _ hi ↦ by simp [Finsupp.indicator, hi])
  · intro i hi hi'
    rw [Finsupp.mem_support_iff, ne_eq, not_not] at hi'
    rw [hi', pow_zero]

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

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

Tactic:
induction p using induction_on with
    | C a => exact aeval_C f a ▸ Subsemiring.subset_closure (Or.inl (Set.mem_range_self a))
    | add p q hp hq => rw [map_add]; exact Subalgebra.add_mem _ hp hq
    | mul_X p n h =>
      simp only [map_mul, aeval_X]
      exact Subalgebra.mul_mem _ h (Algebra.subset_adjoin (Set.mem_range_self n))

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

Goal state before:
pp: case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this✝ : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = s i
this : s ∉ q.support
⊢ s ∈ (p + q).support

Tactic:
simp only [mem_support_iff, ne_eq, coeff_add, not_not] at hs1 ⊢ this

Goal state after:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this✝ : p.support.Nonempty
s : σ →₀ ℕ
hs2 : degreeOf i p = s i
hs1 : ¬coeff s p = 0
this : coeff s q = 0
⊢ ¬coeff s p + coeff s q = 0
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₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
⊢ (eval₂Hom f₁ g₁) p₁ = (eval₂Hom f₁ g₂) p₁

Tactic:
rw [p₁.as_sum]

Goal state after:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
⊢ (eval₂Hom f₁ g₁) (∑ v ∈ p₁.support, (monomial v) (coeff v p₁)) =
    (eval₂Hom f₁ g₂) (∑ v ∈ p₁.support, (monomial v) (coeff v p₁))
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.coeff 0 ≠ 0
⊢ p.trailingCoeff = p.coeff 0

Tactic:
rw [trailingCoeff, (natTrailingDegree_eq_zero.mpr <| .inr h)]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
i : ℕ
r : R
hr : r = 0
⊢ ((monomial i) r).eraseLead = 0

Tactic:
subst r

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
i : ℕ
⊢ ((monomial i) 0).eraseLead = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.leadingCoeff = f.nextCoeff

Tactic:
rw [leadingCoeff, nextCoeff, natDegree_eraseLead h, if_neg,
    eraseLead_coeff_of_ne _ (tsub_lt_self _ _).ne]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < 1

case hnc
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ ¬f.natDegree = 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case neg.a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.coeff f.natTrailingDegree ≠ 0

Tactic:
exact trailingCoeff_nonzero_iff_nonzero.mpr hf

Goal state after: