mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ (∀ (x : M), ∃ a, False ∨ a ≠ 0 ∧ x = 0) ↔ ∀ (x : M), x = 0

Tactic:
false_or,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ (∀ (x : M), ∃ a, a ≠ 0 ∧ x = 0) ↔ ∀ (x : M), x = 0
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: case hsp
R✝ : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst✝⁸ : Semiring R✝
inst✝⁷ : CommSemiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R✝ M
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun i ↦ ↑(bW i)) (surjInv ⋯ ∘ ⇑bQ)
br : ⇑W.mkQ ∘ b ∘ Sum.inr = ⇑bQ
⊢ ⊤ ≤ Submodule.map W.subtype (span R (range fun i ↦ bW i)) ⊔ span R (range (surjInv ⋯ ∘ ⇑bQ))

Tactic:
bW.span_eq,

Goal state after:
case hsp
R✝ : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst✝⁸ : Semiring R✝
inst✝⁷ : CommSemiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R✝ M
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun i ↦ ↑(bW i)) (surjInv ⋯ ∘ ⇑bQ)
br : ⇑W.mkQ ∘ b ∘ Sum.inr = ⇑bQ
⊢ ⊤ ≤ Submodule.map W.subtype ⊤ ⊔ span R (range (surjInv ⋯ ∘ ⇑bQ))
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ IsAtom (K ∙ v)

Tactic:
constructor
  · rw [Submodule.ne_bot_iff]
    exact ⟨v, ⟨mem_span_singleton_self v, hv⟩⟩
  · intro T hT
    by_contra h
    apply hT.2
    change span K {v} ≤ T
    simp_rw [span_singleton_le_iff_mem, ← Ne.eq_def, Submodule.ne_bot_iff] at *
    rcases h with ⟨s, ⟨hs, hz⟩⟩
    rcases mem_span_singleton.1 (hT.1 hs) with ⟨a, rfl⟩
    rcases eq_or_ne a 0 with rfl | h
    · simp only [zero_smul, ne_eq, not_true] at hz
    · rwa [T.smul_mem_iff h] at hs

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
N : Submodule R M
this✝ : Nontrivial R
this : Module.rank R (M ⧸ N) + Module.rank R ↥N ≤ Module.rank R M
⊢ finrank R (M ⧸ N) + finrank R ↥N ≤ finrank R M

Tactic:
rw [← finrank_eq_rank R M, ← finrank_eq_rank R, ← N.finrank_eq_rank] at this

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
N : Submodule R M
this✝ : Nontrivial R
this : ↑(finrank R (M ⧸ N)) + ↑(finrank R ↥N) ≤ ↑(finrank R M)
⊢ finrank R (M ⧸ N) + finrank R ↥N ≤ finrank R M
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
x : E
y : F
H : ∀ (c : R), c • x = 0 → σ c • y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ σ (Classical.choose ⋯) • y = σ c • y

Tactic:
rw [← sub_eq_zero, ← sub_smul, ← RingHom.map_sub]

Goal state after:
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
x : E
y : F
H : ∀ (c : R), c • x = 0 → σ c • y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ σ (Classical.choose ⋯ - c) • y = 0
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
W : Submodule K V
inst✝ : Free K ↥W
m : V
hm : m ∈ W
hm' : ∀ (v : ↥W), ∃ r, r • ⟨m, hm⟩ = v
⊢ ∃ a, (∀ v ∈ W, ∃ r, r • a = v) ∧ a ∈ W

Tactic:
choose f hf using hm'

Goal state after:
case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Submodule K V
inst✝ : Free K ↥W
m : V
hm : m ∈ W
f : ↥W → K
hf : ∀ (v : ↥W), f v • ⟨m, hm⟩ = v
⊢ ∃ a, (∀ v ∈ W, ∃ r, r • a = v) ∧ a ∈ W
Module: Mathlib.LinearAlgebra.LinearPMap

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

pp: case hz
E : Type u_4
inst✝⁵ : AddCommGroup E
F : Type u_5
inst✝⁴ : AddCommGroup F
K : Type u_7
L : Type u_8
inst✝³ : DivisionRing K
inst✝² : DivisionRing L
σ : K →+* L
inst✝¹ : Module K E
inst✝ : Module L F
f : E →ₛₗ.[σ] F
x : E
y : F
hx : x ∉ f.domain
x' : E
hx' : x' ∈ f.domain
c : K
⊢ ↑⟨x', hx'⟩ + ↑⟨c • x, ?m.146⟩ = ↑⟨x' + c • x, ⋯⟩

pp: E : Type u_4
inst✝⁵ : AddCommGroup E
F : Type u_5
inst✝⁴ : AddCommGroup F
K : Type u_7
L : Type u_8
inst✝³ : DivisionRing K
inst✝² : DivisionRing L
σ : K →+* L
inst✝¹ : Module K E
inst✝ : Module L F
f : E →ₛₗ.[σ] F
x : E
y : F
hx : x ∉ f.domain
x' : E
hx' : x' ∈ f.domain
c : K
⊢ c • x ∈ (mkSpanSingleton x y ⋯).domain

Tactic:
mkSpanSingleton'_apply

Goal state after:
E : Type u_4
inst✝⁵ : AddCommGroup E
F : Type u_5
inst✝⁴ : AddCommGroup F
K : Type u_7
L : Type u_8
inst✝³ : DivisionRing K
inst✝² : DivisionRing L
σ : K →+* L
inst✝¹ : Module K E
inst✝ : Module L F
f : E →ₛₗ.[σ] F
x : E
y : F
hx : x ∉ f.domain
x' : E
hx' : x' ∈ f.domain
c : K
⊢ ↑f ⟨x', hx'⟩ + σ c • y = ↑f ⟨x', hx'⟩ + σ c • y

case hz
E : Type u_4
inst✝⁵ : AddCommGroup E
F : Type u_5
inst✝⁴ : AddCommGroup F
K : Type u_7
L : Type u_8
inst✝³ : DivisionRing K
inst✝² : DivisionRing L
σ : K →+* L
inst✝¹ : Module K E
inst✝ : Module L F
f : E →ₛₗ.[σ] F
x : E
y : F
hx : x ∉ f.domain
x' : E
hx' : x' ∈ f.domain
c : K
⊢ ↑⟨x', hx'⟩ + ↑⟨c • x, ?m.146⟩ = ↑⟨x' + c • x, ⋯⟩

E : Type u_4
inst✝⁵ : AddCommGroup E
F : Type u_5
inst✝⁴ : AddCommGroup F
K : Type u_7
L : Type u_8
inst✝³ : DivisionRing K
inst✝² : DivisionRing L
σ : K →+* L
inst✝¹ : Module K E
inst✝ : Module L F
f : E →ₛₗ.[σ] F
x : E
y : F
hx : x ∉ f.domain
x' : E
hx' : x' ∈ f.domain
c : K
⊢ c • x ∈ (mkSpanSingleton x y ⋯).domain
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)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
⊢ ∃ f, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c

Tactic:
use { toFun := f, map_add' := ?_, map_smul' := ?_ }, ?_

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
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 : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
⊢ ∀ (x y : ↥(sSup (domain '' c))), f (x + y) = f x + f y

case w.refine_2
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 : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
⊢ ∀ (m : R) (x : ↥(sSup (domain '' c))), f (m • x) = σ m • f x

case h
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 : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
⊢ { domain := sSup (domain '' c), toFun := { toFun := f, map_add' := ?w.refine_1, map_smul' := ?w.refine_2 } } ∈
    upperBounds c
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case grade1
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x : X
⊢ ι R x ∈ S

Tactic:
exact Algebra.subset_adjoin (Set.mem_range_self _)

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

Goal state before:
pp: case mp
n : ℕ
⊢ n.minFac = 1 → n = 1

Tactic:
intro h
    by_contra hn
    have := minFac_prime hn
    rw [h] at this
    exact not_prime_one this

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

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
v : ℕ
hv : v ≠ 1
hr : CharP R v
h : ↑1 = 0
⊢ v = 1

Tactic:
CharP.cast_eq_zero_iff _ v,

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
v : ℕ
hv : v ≠ 1
hr : CharP R v
h : v ∣ 1
⊢ v = 1
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_fst : E
x_snd : F
⊢ (x_fst, x_snd) ∈ g.toLinearPMap.graph ↔ (x_fst, x_snd) ∈ g

Tactic:
constructor <;> intro hx

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
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

case mpr
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
⊢ (x_fst, x_snd) ∈ g.toLinearPMap.graph
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:
rw [List.prod_cons, List.map_cons, List.sum_cons]
    grw [sup_support_coeff_mul_le degbm, sup_support_list_prod_le degb0 degbm]

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

Goal state before:
pp: case h₀
R : Type u
inst✝ : Semiring R
r : R
n k b✝ : ℕ
⊢ b✝ ∈ range (n + 1) → b✝ ≠ k → (X ^ b✝).coeff k * r ^ (n - b✝) * ↑(n.choose b✝) = 0

Tactic:
_

Goal state after:
case h₀
R : Type u
inst✝ : Semiring R
r : R
n k b✝ : ℕ
a✝ : b✝ ∈ range (n + 1)
⊢ b✝ ≠ k → (X ^ b✝).coeff k * r ^ (n - b✝) * ↑(n.choose b✝) = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R' : Type u_2
A : Type u_3
B : Type u_5
inst✝² : Ring R'
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
f : R'[A]
⊢ supDegree D (-f) = supDegree D f

Tactic:
simp [supDegree]

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

Goal state before:
pp: case neg
R : Type u
a : R
inst✝ : Semiring R
h : ¬a = 0
⊢ (C a).degree ≤ 0

Tactic:
degree_C h

Goal state after:
case neg
R : Type u
a : R
inst✝ : Semiring R
h : ¬a = 0
⊢ 0 ≤ 0
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✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
⊢ supDegree D 0 = ⊥

Tactic:
simp [supDegree]

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
h : ∀ (i : ℕ), r ∣ φ.coeff i
⊢ C r ∣ φ

Tactic:
choose c hc using h

Goal state after:
case mpr
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
⊢ C r ∣ φ
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.nextCoeff = 0 ↔ p.natDegree = 0 ∨ 0 < p.natDegree ∧ p.coeff (p.natDegree - 1) = 0

Tactic:
by
  simp [nextCoeff, or_iff_not_imp_left, pos_iff_ne_zero]; simp_all

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

Goal state before:
pp: case pos
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 : Fin n
⊢ i ∈ univ → f (↑i) (coeff 0 ↑i) = 0

Tactic:
_

Goal state after:
case pos
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 : Fin n
a✝ : i ∈ univ
⊢ f (↑i) (coeff 0 ↑i) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ ((monomial n) 1).degree = ↑n

Tactic:
degree_monomial _ (one_ne_zero' R)

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ ↑n = ↑n
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case bot
m : WithBot ℕ
⊢ ⊥ + m = 0 ↔ ⊥ = 0 ∧ m = 0

pp: case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 0 ↔ ↑a✝ = 0 ∧ m = 0

Tactic:
· simp [WithBot.bot_add]

Goal state after:
case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 0 ↔ ↑a✝ = 0 ∧ m = 0
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case bot
m : WithBot ℕ
⊢ ⊥ + m = 2 ↔ ⊥ = 0 ∧ m = 2 ∨ ⊥ = 1 ∧ m = 1 ∨ ⊥ = 2 ∧ m = 0

pp: case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 2 ↔ ↑a✝ = 0 ∧ m = 2 ∨ ↑a✝ = 1 ∧ m = 1 ∨ ↑a✝ = 2 ∧ m = 0

Tactic:
· simp [WithBot.bot_add]

Goal state after:
case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 2 ↔ ↑a✝ = 0 ∧ m = 2 ∨ ↑a✝ = 1 ∧ m = 1 ∨ ↑a✝ = 2 ∧ m = 0
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case bot
m : WithBot ℕ
⊢ ⊥ + m = 3 ↔ ⊥ = 0 ∧ m = 3 ∨ ⊥ = 1 ∧ m = 2 ∨ ⊥ = 2 ∧ m = 1 ∨ ⊥ = 3 ∧ m = 0

pp: case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 3 ↔ ↑a✝ = 0 ∧ m = 3 ∨ ↑a✝ = 1 ∧ m = 2 ∨ ↑a✝ = 2 ∧ m = 1 ∨ ↑a✝ = 3 ∧ m = 0

Tactic:
· simp [WithBot.bot_add]

Goal state after:
case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 3 ↔ ↑a✝ = 0 ∧ m = 3 ∨ ↑a✝ = 1 ∧ m = 2 ∨ ↑a✝ = 2 ∧ m = 1 ∨ ↑a✝ = 3 ∧ m = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
by
    rw [degree_mul' h, Nat.cast_add, degree_eq_natDegree hp, degree_eq_natDegree hq]

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

Goal state before:
pp: n : ℕ
⊢ 0 ≤ n

Tactic:
exact n.zero_le

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

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

Tactic:
mul_ne_zero_iff

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p ≠ 0 ∧ q ≠ 0
⊢ p.natDegree ≤ (p * q).natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p * q ≠ 0
⊢ p.degree ≤ (p * q).degree

Tactic:
mul_ne_zero_iff

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p ≠ 0 ∧ q ≠ 0
⊢ p.degree ≤ (p * q).degree
Module: Mathlib.Algebra.Polynomial.Eval.Degree

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

Tactic:
refine natDegree_pow_le.trans_lt ?_

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ b * q.natDegree < p.natDegree * q.natDegree
Module: Mathlib.Algebra.Polynomial.Eval.Degree

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

Tactic:
_

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
hr : r ∈ nonZeroDivisors R
⊢ p.comp (C r * X) = 0 ↔ p = 0

Tactic:
simp_rw [ext_iff]
  refine forall_congr' fun n ↦ ?_
  rw [comp_C_mul_X_coeff, coeff_zero, mul_right_mem_nonZeroDivisors_eq_zero_iff (pow_mem hr _)]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
a : R
⊢ C a * X s = (monomial (Finsupp.single s 1)) a

Tactic:
by
  rw [← C_mul_X_pow_eq_monomial, pow_one]

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
⊢ (X n).support = {Finsupp.single n 1}

Tactic:
by
  classical rw [X, support_monomial, if_neg]; exact one_ne_zero

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d₀ : σ →₀ ℕ
h : ∀ d ∈ φ.support, d = d₀
⊢ φ = (monomial d₀) (coeff d₀ φ)

Tactic:
ext d
  rcases eq_or_ne d d₀ with rfl | hd
  · rw [coeff_monomial, if_pos rfl]
  · rw [notMem_support_iff.mp fun hmem ↦ hd (h d hmem), coeff_monomial, if_neg fun e ↦ hd e.symm]

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

Goal state before:
pp: R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
⊢ (eval₂Hom f g) φ = 0

Tactic:
rw [φ.as_sum, map_sum]
  refine Finset.sum_eq_zero fun d hd => ?_
  obtain ⟨i, hi, hgi⟩ : ∃ i ∈ d.support, g i = 0 := h d (Finsupp.mem_support_iff.mp hd)
  rw [eval₂Hom_monomial, Finsupp.prod, Finset.prod_eq_zero hi, mul_zero]
  rw [hgi, zero_pow]
  rwa [← Finsupp.mem_support_iff]

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

Goal state before:
pp: case pos
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
h0 : constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ (f (coeff d p) * d.prod fun i k ↦ g i ^ k) = 0

pp: case neg.h₀
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
h0 : ¬constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
⊢ (f (coeff d p) * d.prod fun i k ↦ g i ^ k) = 0

pp: case neg.h₁
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
h0 : ¬constantCoeff p = 0
⊢ 0 ∉ p.support → (f (coeff 0 p) * Finsupp.prod 0 fun i k ↦ g i ^ k) = 0

Tactic:
on_goal 3 =>
    rw [constantCoeff_eq, coeff, ← Ne, ← Finsupp.mem_support_iff] at h0
    intro
    contradiction

Goal state after:
case pos
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
h0 : constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ (f (coeff d p) * d.prod fun i k ↦ g i ^ k) = 0

case neg.h₀
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
h0 : ¬constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
⊢ (f (coeff d p) * d.prod fun i k ↦ g i ^ k) = 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case refine_2
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
i : σ
hip : i ∈ p.vars
⊢ i ∈ p.vars →
    ((rename f).comp (aeval fun i ↦ Option.elim' 0 X (partialInv f i)).toRingHom) (X i) =
      (RingHom.id (MvPolynomial σ R)) (X i)

Tactic:
_

Goal state after:
case refine_2
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
i : σ
hip a✝ : i ∈ p.vars
⊢ ((rename f).comp (aeval fun i ↦ Option.elim' 0 X (partialInv f i)).toRingHom) (X i) =
    (RingHom.id (MvPolynomial σ R)) (X i)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
o : ℕ
pn : p.natDegree ≤ n
mno : m * n ≤ o
⊢ (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0

Tactic:
rcases eq_or_ne o (m * n) with rfl | h

Goal state after:
case inl
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
mno : m * n ≤ m * n
⊢ (p ^ m).coeff (m * n) = if m * n = m * n then p.coeff n ^ m else 0

case inr
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
o : ℕ
pn : p.natDegree ≤ n
mno : m * n ≤ o
h : o ≠ m * n
⊢ (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case refine_2
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff n = p.coeff n

Tactic:
obtain _ | _ | n := n

Goal state after:
case refine_2.zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff 0 = p.coeff 0

case refine_2.succ.zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff (0 + 1) = p.coeff (0 + 1)

case refine_2.succ.succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff (n + 1 + 1) = p.coeff (n + 1 + 1)
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
⊢ r ≠ 0 → n ≤ N → eval₂ i (⅟x) (reflect N (C r * X ^ n)) * x ^ N = eval₂ i x (C r * X ^ n)

Tactic:
_

Goal state after:
case refine_2
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
⊢ n ≤ N → eval₂ i (⅟x) (reflect N (C r * X ^ n)) * x ^ N = eval₂ i x (C r * X ^ n)
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
⊢ ¬(False ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0))

Tactic:
false_or,

Goal state after:
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 = C (q.coeff 0))
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
· rwa [hp.leadingCoeff, one_mul, leadingCoeff_ne_zero]

Goal state after: