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

Goal state before:
pp: case hli.hf
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 ⇑bW

pp: case hli.hg
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 (Submodule.Quotient.mk ∘ surjInv ⋯ ∘ ⇑bQ)

Tactic:
· exact bW.linearIndependent

Goal state after:
case hli.hg
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 (Submodule.Quotient.mk ∘ surjInv ⋯ ∘ ⇑bQ)
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : NonUnitalRing A
inst✝¹ : Module R A
inst✝ : Star A
S T : NonUnitalStarSubalgebra R A
h : S.toNonUnitalSubring = T.toNonUnitalSubring
x : A
⊢ x ∈ S ↔ x ∈ T

Tactic:
by rw [← mem_toNonUnitalSubring, ← mem_toNonUnitalSubring, h]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ finrank R M = 0 ↔ ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0

Tactic:
rw [← rank_eq_zero_iff (R := R), ← finrank_eq_rank]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ finrank R M = 0 ↔ ↑(finrank R M) = 0
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
⊢ ∃ n b i j, i ≠ j ∧ ↑v = b i ∧ f = b.coord j

Tactic:
set n := insert w s

Goal state after:
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
⊢ ∃ n b i j, i ≠ j ∧ ↑v = b i ∧ f = b.coord j
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
⊢ Module.rank K ↥s = 1 ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ s ≤ K ∙ v₀

Tactic:
rank_eq_one_iff,

Goal state after:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
⊢ (∃ v₀, v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ r, r • v₀ = v) ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ s ≤ K ∙ v₀
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case refine_1
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
⊢ K ∙ v = S

Tactic:
have : K ∙ v ≠ ⊥ := by
      rw [Submodule.ne_bot_iff]
      exact ⟨v, mem_span_singleton_self v, hv_ne⟩

Goal state after:
case refine_1
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
this : K ∙ v ≠ ⊥
⊢ K ∙ v = S
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✝¹ + 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:
change liftFun R X f _ + liftFun R X f _ = _
        simp only [*]
        rfl

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✝ + 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✝ + 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:
change liftFun R X f _ + liftFun R X f _ = _
        simp only [*]
        rfl

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 (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 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:
change liftFun R X f _ + liftFun R X f _ = _
        simp only [*]
        rfl

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 (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.LinearAlgebra.LinearPMap

Goal state before:
pp: case inr
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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
⊢ ∃ f, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c

Tactic:
have P : ∀ x : ↥(sSup (domain '' c)), { p : c // (x : E) ∈ p.val.domain } := by
    rintro x
    apply Classical.indefiniteDescription
    have := (mem_sSup_of_directed (cne.image _) hdir).1 x.2
    rwa [Set.exists_mem_image, ← bex_def, SetCoe.exists'] at this

Goal state after:
case inr
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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
⊢ ∃ f, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ mdvd : m ∣ p
k : ℕ
e : p = m * k
h✝ : mdvd = ⋯
hk : k ≤ p.sqrt
⊢ False

Tactic:
rw [mul_comm] at e

Goal state after:
case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ mdvd : m ∣ p
k : ℕ
e✝ : p = m * k
e : p = k * m
h✝ : mdvd = ⋯
hk : k ≤ p.sqrt
⊢ False
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
⊢ (∃ y, (↑y, ↑f y) = (fst✝, snd✝)) ↔ ∃ y, ↑y = fst✝ ∧ ↑f y = snd✝

Tactic:
Prod.mk_inj

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

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
d : ℕ
⊢ (1 + X) ^ d - X ^ d = ∑ i ∈ range d, d.choose i • X ^ i

Tactic:
by
  ext i
  simp [Polynomial.coeff_one_add_X_pow]
  split_ifs <;> simp_all [Nat.choose_eq_zero_of_lt, lt_iff_le_and_ne]

Goal state after:
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) = p.sum f

Tactic:
sum_over_range' _ hf n ((natDegree_lt_iff_degree_lt hp).mpr hn),

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, f (↑i) (p.coeff ↑i) = ∑ a ∈ range n, f a (p.coeff a)
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case refine_2
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p.natDegree, q.natDegree) ∉ antidiagonal (p.natDegree + q.natDegree) →
    p.coeff (p.natDegree, q.natDegree).1 * q.coeff (p.natDegree, q.natDegree).2 = 0

Tactic:
intro H
        exfalso
        apply H
        rw [mem_antidiagonal]

Goal state after:
Module: Mathlib.Data.Nat.WithBot

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

Tactic:
cases n
  · simp
  cases m
  · simp [WithBot.add_bot]
  simp [← WithBot.coe_add, Nat.add_eq_one_iff]

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

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

Tactic:
by_cases hr : r = 0

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
hr : r = 0
⊢ (C r * p).leadingCoeff = r

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
hr : ¬r = 0
⊢ (C r * p).leadingCoeff = r
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ p.coeff (Function.invFun D (supDegree D p)) + q.coeff (Function.invFun D (supDegree D p)) = leadingCoeff D p

Tactic:
← leadingCoeff,

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ leadingCoeff D p + q.coeff (Function.invFun D (supDegree D p)) = leadingCoeff D p
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬(p - q).coeff (Function.invFun D (supDegree D (p - q))) = 0
h : supDegree D (p - q) = supDegree D p
⊢ p.coeff (Function.invFun D (supDegree D p)) - q.coeff (Function.invFun D (supDegree D p)) = 0

Tactic:
← leadingCoeff,

Goal state after:
case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬(p - q).coeff (Function.invFun D (supDegree D (p - q))) = 0
h : supDegree D (p - q) = supDegree D p
⊢ leadingCoeff D p - q.coeff (Function.invFun D (supDegree D p)) = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬(p - q).coeff (Function.invFun D (supDegree D (p - q))) = 0
h : supDegree D (p - q) = supDegree D p
⊢ leadingCoeff D p - q.coeff (Function.invFun D (supDegree D q)) = 0

Tactic:
← leadingCoeff,

Goal state after:
case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬(p - q).coeff (Function.invFun D (supDegree D (p - q))) = 0
h : supDegree D (p - q) = supDegree D p
⊢ leadingCoeff D p - leadingCoeff D q = 0
Module: Mathlib.Algebra.Polynomial.Degree.Units

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
u : R[X]ˣ
⊢ (↑u).coeff (↑u).natDegree ≠ 0

Tactic:
← leadingCoeff,

Goal state after:
R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
u : R[X]ˣ
⊢ (↑u).leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

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

Tactic:
leadingCoeff_add_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha,

Goal state after:
R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X ^ 2).leadingCoeff = a
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
⊢ ↑n ≠ ⊥

Tactic:
exact WithBot.coe_ne_bot

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

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

Tactic:
simp only [hp, zero_mul, leadingCoeff_zero]

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

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
⊢ f.coeff i = ((monomial n) (f.coeff n)).coeff i

Tactic:
by_cases hi : i = n

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : i = n
⊢ f.coeff i = ((monomial n) (f.coeff n)).coeff i

case neg
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ f.coeff i = ((monomial n) (f.coeff n)).coeff i
Module: Mathlib.Algebra.Polynomial.Eval.Degree

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

Tactic:
← leadingCoeff,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : (map f p).leadingCoeff = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ p = 0
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:
by
    simpa only [Pi.toLex_apply, Function.comp_apply, Equiv.swap_apply_left] using h₂

Goal state after:
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
h : f = g
⊢ f.neLocus f = ∅

Tactic:
simp only [neLocus, Ne, not_true, Finset.filter_false]

Goal state after:
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₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p q : MvPolynomial σ R),
    (∀ {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 (q * (monomial s) a) = eval₂ f g q * f a * s.prod fun n e ↦ g n ^ e) →
        ∀ {s : σ →₀ ℕ} {a : R},
          eval₂ f g ((p + q) * (monomial s) a) = eval₂ f g (p + q) * f a * s.prod fun n e ↦ g n ^ e

Tactic:
intro p q ih_p ih_q

Goal state after:
case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
p q : MvPolynomial σ R
ih_p : ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e
ih_q : ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (q * (monomial s) a) = eval₂ f g q * f a * s.prod fun n e ↦ g n ^ e
⊢ ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g ((p + q) * (monomial s) a) = eval₂ f g (p + q) * f a * s.prod fun n e ↦ g n ^ e
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
c : R
⊢ c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = coeff n p

Tactic:
by
  simp [coeffs, eq_comm, (Finset.mem_image)]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ ≃ τ
p : MvPolynomial σ R
⊢ (rename ⇑f.symm) ((rename ⇑f) p) = p

Tactic:
by rw [rename_rename, f.symm_comp_self, rename_id_apply]

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

Goal state before:
pp: case add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial (↥s) R
t : Finset σ
q : MvPolynomial (↥t) R
⊢ ∃ s_1 q_1, (rename Subtype.val) p + (rename Subtype.val) q = (rename Subtype.val) q_1

Tactic:
refine ⟨s ∪ t, ⟨?_, ?_⟩⟩

Goal state after:
case add.refine_1
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial (↥s) R
t : Finset σ
q : MvPolynomial (↥t) R
⊢ MvPolynomial (↥(s ∪ t)) R

case add.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial (↥s) R
t : Finset σ
q : MvPolynomial (↥t) R
⊢ (rename Subtype.val) p + (rename Subtype.val) q = (rename Subtype.val) ?add.refine_1
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
⊢ (-p).degrees = p.degrees

Tactic:
rw [degrees, support_neg]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
⊢ (p.support.sup fun s ↦ toMultiset s) = p.degrees
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 : ℤ
⊢ c n = ↑n

Tactic:
exact eq_intCast c n

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 p q : MvPolynomial R ℤ
hp : eval₂ c (⇑f ∘ X) p = f p
hq : eval₂ c (⇑f ∘ X) q = f q
⊢ eval₂ c (⇑f ∘ X) (p + q) = f (p + q)

Tactic:
rw [eval₂_add, hp, hq]

Goal state after:
S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p q : MvPolynomial R ℤ
hp : eval₂ c (⇑f ∘ X) p = f p
hq : eval₂ c (⇑f ∘ X) q = f q
⊢ f p + f q = f (p + q)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : q.natDegree = 0
⊢ p.natDegree * q.natDegree ≤ (p.comp q).natDegree

Tactic:
simp [hq]

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

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

Tactic:
by_cases hr : r = 0

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

case neg
R : Type u_1
inst✝ : Semiring R
i : ℕ
r : R
hr : ¬r = 0
⊢ ((monomial i) r).eraseLead = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
⊢ ¬eval (q.coeff 0) p = 0 ∨ ¬q.degree ≤ 0

Tactic:
simp [hq]

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

Goal state before:
pp: case pos
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp0 : p = 0
⊢ Irreducible (p * C p.leadingCoeff⁻¹) ↔ Irreducible p

Tactic:
simp [hp0]

Goal state after: