mathlib-initiative/mathlib-tactics huggingface dataset:
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 ⋯
this : span K (Set.range ⇑(Basis.ofVectorSpace K ↥S)) = ⊤
⊢ S = Submodule.map S.subtype (span K (Basis.ofVectorSpaceIndex K ↥S))

Tactic:
Basis.coe_ofVectorSpace,

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 ⋯
this : span K (Set.range Subtype.val) = ⊤
⊢ S = Submodule.map S.subtype (span K (Basis.ofVectorSpaceIndex K ↥S))
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
inst✝ : Free K V
⊢ Module.rank K V ≤ 1 ↔ ∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v

Tactic:
obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := K) (M := V)
  constructor
  · intro hd
    rw [← b.mk_eq_rank'', le_one_iff_subsingleton] at hd
    rcases isEmpty_or_nonempty κ with hb | ⟨⟨i⟩⟩
    · use 0
      have h' : ∀ v : V, v = 0 := by
        simpa [range_eq_empty, Submodule.eq_bot_iff] using b.span_eq.symm
      intro v
      simp [h' v]
    · use b i
      have h' : K ∙ b i = ⊤ :=
        (subsingleton_range b).eq_singleton_of_mem (mem_range_self i) ▸ b.span_eq
      intro v
      have hv : v ∈ (⊤ : Submodule K V) := mem_top
      rwa [← h', mem_span_singleton] at hv
  · rintro ⟨v₀, hv₀⟩
    have h : K ∙ v₀ = ⊤ := by
      ext
      simp [mem_span_singleton, hv₀]
    rw [← rank_top, ← h]
    refine (rank_span_le _).trans_eq ?_
    simp

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
ι : Type u_1
inst✝ : Unique ι
⊢ finrank K V = 1 → Nonempty (Basis ι K V)

pp: case mpr
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
ι : Type u_1
inst✝ : Unique ι
⊢ Nonempty (Basis ι K V) → finrank K V = 1

Tactic:
· intro h
    exact ⟨Module.basisUnique ι h⟩

Goal state after:
case mpr
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
ι : Type u_1
inst✝ : Unique ι
⊢ Nonempty (Basis ι K V) → finrank K V = 1
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case refine_1
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
⊢ Module.rank F ↥⊥ ≤ 1

Tactic:
have := lift_rank_range_le (Algebra.linearMap F E)
    rwa [← one_eq_range, rank_self, lift_one, lift_le_one_iff,
      ← Algebra.toSubmodule_bot, rank_toSubmodule] at this

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case zero_add
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✝ : Pre R X
⊢ liftFun R X f (0 + a✝) = liftFun R X f a✝

Tactic:
change algebraMap _ _ _ + liftFun R X f _ = liftFun R X f _
        simp

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

Goal state before:
pp: p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ m → m < p → ¬m ∣ p
l : m < p
d : m ∣ p
⊢ m = 1

Tactic:
by
          rcases m with (_ | _ | m)
          · omega
          · rfl
          · exact (h (le_add_left 2 m) l).elim d

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case left
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 g : E →ₗ.[R] F
h : f.graph ≤ g.graph
⊢ f.domain ≤ g.domain

pp: case right
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 g : E →ₗ.[R] F
h : f.graph ≤ g.graph
⊢ ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y

Tactic:
· intro x hx
    rw [mem_domain_iff] at hx ⊢
    obtain ⟨y, hx⟩ := hx
    use y
    exact h hx

Goal state after:
case right
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 g : E →ₗ.[R] F
h : f.graph ≤ g.graph
⊢ ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_5
inst✝⁴ : AddCommGroup F
inst✝³ : Module S F
G : Type u_6
inst✝² : AddCommGroup G
inst✝¹ : Module T G
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
v w : ↥(map (LinearMap.fst R E F) g)
⊢ valFromGraph hg ⋯ = valFromGraph hg ⋯ + valFromGraph hg ⋯

Tactic:
have hadd := (g.map (LinearMap.fst R E F)).add_mem v.2 w.2

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_5
inst✝⁴ : AddCommGroup F
inst✝³ : Module S F
G : Type u_6
inst✝² : AddCommGroup G
inst✝¹ : Module T G
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
v w : ↥(map (LinearMap.fst R E F) g)
hadd : ↑v + ↑w ∈ map (LinearMap.fst R E F) g
⊢ valFromGraph hg ⋯ = valFromGraph hg ⋯ + valFromGraph hg ⋯
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : a ∈ s
hfsa : IsMinOn f s a
b : β
⊢ b ≤ f a ↔ b ∈ lowerBounds {x | ∃ x_1 ∈ s, f x_1 = x}

Tactic:
simp only [mem_lowerBounds, mem_ofPred_eq, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Goal state after:
α : Type u
β : Type v
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : a ∈ s
hfsa : IsMinOn f s a
b : β
⊢ b ≤ f a ↔ ∀ a ∈ s, b ≤ f a
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: 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
hx_fst : x_fst ∈ map (LinearMap.fst R E F) g
⊢ ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑g.toLinearPMap y = (x_fst, x_snd).2

Tactic:
refine ⟨⟨x_fst, hx_fst⟩, Subtype.coe_mk x_fst hx_fst, ?_⟩

Goal state after:
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
hx_fst : x_fst ∈ map (LinearMap.fst R E F) g
⊢ ↑g.toLinearPMap ⟨x_fst, hx_fst⟩ = (x_fst, x_snd).2
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
f : E →ₗ.[R] F
hf : f.toFun.ker = ⊥
y : E
hv : ∃ y_1, ↑y_1 = y ∧ ↑f y_1 = 0
⊢ (0, y).2 = 0

Tactic:
rcases hv with ⟨z, rfl, hz⟩

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
f : E →ₗ.[R] F
hf : f.toFun.ker = ⊥
z : ↥f.domain
hz : ↑f z = 0
⊢ (0, ↑z).2 = 0
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Monoid M
f : A →ₐ[R] B
x : A[M]
m : M
⊢ ((mapAlgHom M f) x).coeff m = f (x.coeff m)

Tactic:
simp [mapAlgHom]

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]
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).degree = p.degree + q.degree

Tactic:
degree_mul

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p ≠ 0
hq : q ≠ 0
⊢ p.degree + q.degree = p.degree + q.degree
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: case pos
R : Type u
inst✝⁴ : Semiring R
p : R[X]
S : Type u_1
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : Module S R
inst✝ : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : p = 0
⊢ (a • p).natDegree = p.natDegree

Tactic:
simp only [hp, smul_zero]

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

Goal state before:
pp: case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 0 ↔ ↑a✝ = 0 ∧ ⊥ = 0

pp: case coe.coe
a✝¹ a✝ : ℕ
⊢ ↑a✝¹ + ↑a✝ = 0 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 0

Tactic:
· simp [WithBot.add_bot]

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

Goal state before:
pp: case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 1 ↔ ↑a✝ = 0 ∧ ⊥ = 1 ∨ ↑a✝ = 1 ∧ ⊥ = 0

pp: case coe.coe
a✝¹ a✝ : ℕ
⊢ ↑a✝¹ + ↑a✝ = 1 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 1 ∨ ↑a✝¹ = 1 ∧ ↑a✝ = 0

Tactic:
· simp [WithBot.add_bot]

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

Goal state before:
pp: case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 2 ↔ ↑a✝ = 0 ∧ ⊥ = 2 ∨ ↑a✝ = 1 ∧ ⊥ = 1 ∨ ↑a✝ = 2 ∧ ⊥ = 0

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

Tactic:
· simp [WithBot.add_bot]

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

Goal state before:
pp: case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 3 ↔ ↑a✝ = 0 ∧ ⊥ = 3 ∨ ↑a✝ = 1 ∧ ⊥ = 2 ∨ ↑a✝ = 2 ∧ ⊥ = 1 ∨ ↑a✝ = 3 ∧ ⊥ = 0

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

Tactic:
· simp [WithBot.add_bot]

Goal state after:
case coe.coe
a✝¹ a✝ : ℕ
⊢ ↑a✝¹ + ↑a✝ = 3 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 3 ∨ ↑a✝¹ = 1 ∧ ↑a✝ = 2 ∨ ↑a✝¹ = 2 ∧ ↑a✝ = 1 ∨ ↑a✝¹ = 3 ∧ ↑a✝ = 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✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D p < supDegree D q
⊢ leadingCoeff D (p + q) = leadingCoeff D q

Tactic:
by
  rw [add_comm, leadingCoeff_add_eq_left h]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ 0 ≤ p.degree ↔ p ≠ 0

Tactic:
← not_lt,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ¬p.degree < 0 ↔ p ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
this✝ : Nontrivial R
this : p.leadingCoeff * X.leadingCoeff ≠ 0
⊢ ↑p.natDegree < ↑p.natDegree + ↑1

Tactic:
← Nat.cast_add

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
this✝ : Nontrivial R
this : p.leadingCoeff * X.leadingCoeff ≠ 0
⊢ ↑p.natDegree < ↑(p.natDegree + 1)
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
h✝ : Function.Surjective (map f)
s : S
p : R[X]
h : map f p = C s
⊢ f (p.coeff 0) = s

Tactic:
simpa using congr(coeff $h 0)

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

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

Tactic:
· rw [leadingCoeff_mul']
      exact mul_ne_zero (mt leadingCoeff_eq_zero.1 hp) (mt leadingCoeff_eq_zero.1 hq)

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
i : ι
inst✝ : NoMaxOrder (β i)
a : Lex ((i : ι) → β i)
b : β i
hb : a i < b
⊢ (fun {i} x1 x2 ↦ x1 < x2) (a i) (Function.update a i b i)

Tactic:
Function.update_self i b

Goal state after:
ι : Type u_1
β : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
i : ι
inst✝ : NoMaxOrder (β i)
a : Lex ((i : ι) → β i)
b : β i
hb : a i < b
⊢ (fun {i} x1 x2 ↦ x1 < x2) (a i) b
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
⊢ p ∣ f.coeff i * z ^ i

Tactic:
by
  by_cases hi : i ∈ f.support
  · rw [eval, eval₂_eq_sum, sum_def] at dvd_eval
    rw [← Finset.insert_erase hi, Finset.sum_insert (Finset.notMem_erase _ _)] at dvd_eval
    refine (dvd_add_left ?_).mp dvd_eval
    apply Finset.dvd_sum
    intro j hj
    exact dvd_terms j (Finset.ne_of_mem_erase hj)
  · convert! dvd_zero p
    rw [notMem_support_iff] at hi
    simp [hi]

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

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

Tactic:
hi'

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → ℕ
t : Finset σ
i : σ
hi : i ∈ t
hi' : i ∉ (Finsupp.indicator t fun i x_1 ↦ x i).support
⊢ X i ^ (Finsupp.indicator t fun i x_1 ↦ x i) i = 1
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
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:
· rw [add_comm]
    exact support_sdiff_support_subset_support_add q p

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:
rename_rename,

Goal state after:
σ : 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 ∘ ⇑f)) p = p
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) ((rename ⇑f.symm) p) = p

Tactic:
rename_rename,

Goal state after:
σ : 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 ∘ ⇑f.symm)) p = p
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
⊢ ∃ n f, ∃ (_ : Injective f), ∃ q_1, (rename Subtype.val) q = (rename f) q_1

Tactic:
let n := Fintype.card { x // x ∈ s }

Goal state after:
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset σ
q : MvPolynomial (↥s) R
n : ℕ := Fintype.card ↥s
⊢ ∃ n f, ∃ (_ : Injective f), ∃ q_1, (rename Subtype.val) q = (rename f) q_1
Module: Mathlib.Algebra.MvPolynomial.Degrees

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

Tactic:
rw [pow_zero, mul_one]

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

Goal state before:
pp: case neg
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
⊢ (f (coeff 0 p) * Finsupp.prod 0 fun i k ↦ g i ^ k) = f (constantCoeff p)

Tactic:
Finsupp.prod_zero_index,

Goal state after:
case neg
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
⊢ f (coeff 0 p) * 1 = f (constantCoeff p)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : a * ai = 1
⊢ p.natDegree = (p * 1).natDegree

Tactic:
by nth_rw 1 [← mul_one p]

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

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

Tactic:
by_cases nd : n = q.natDegree

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : n = q.natDegree
⊢ (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n

case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case zero.succ
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
by_cases g0 : g = 0

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : g = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

case neg
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
a : R
ha : a ≠ 0
b : R
hnext : (C a * X + C b).nextCoeff = 0
⊢ (C a * X + C b).eraseLead = 0

Tactic:
nextCoeff_C_mul_X_add_C ha

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
a : R
ha : a ≠ 0
b : R
hnext : b = 0
⊢ (C a * X + C b).eraseLead = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
⊢ ¬(map f p).degree = ⊥

Tactic:
h2,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
⊢ ¬p.degree = ⊥
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h : P.coeff (dP + 1) = 0
⊢ (if P.natDegree + 1 = 0 then 0 else ((X - C x) * P).coeff P.natDegree) ≠ 0

Tactic:
hdP,

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h : P.coeff (dP + 1) = 0
⊢ (if dP + 2 + 1 = 0 then 0 else ((X - C x) * P).coeff (dP + 2)) ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case refine_1
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
h : p.coeff 1 = 0
⊢ False

Tactic:
rw [← hp, coeff_natDegree, leadingCoeff_eq_zero] at h
    simp_all

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

Goal state before:
pp: case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
j : Option S₁ →₀ ℕ
r : R
n : Option S₁ →₀ ℕ
hj : ¬j = n
⊢ (if j none = n none then if j.some = n.some then r else 0 else 0) = 0

Tactic:
simp only [ite_eq_right_iff]

Goal state after:
case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
j : Option S₁ →₀ ℕ
r : R
n : Option S₁ →₀ ℕ
hj : ¬j = n
⊢ j none = n none → j.some = n.some → r = 0
Module: Mathlib.Algebra.Polynomial.Monic

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

Tactic:
by
  unfold Monic
  nontriviality
  rw [leadingCoeff_mul' _] <;> simp [leadingCoeff_C b, hp]

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

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

Tactic:
by
  unfold Monic
  nontriviality
  rw [leadingCoeff_mul' _] <;> simp [leadingCoeff_C b, hp]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.leadingCoeff = f.trailingCoeff

Tactic:
rw [leadingCoeff, reverse_natDegree, ← revAt_le f.natTrailingDegree_le_natDegree,
    coeff_reverse, revAt_invol, trailingCoeff]

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

Goal state before:
pp: case neg
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
⊢ (f * g).reverse = f.reverse * g.reverse

Tactic:
by_cases g0 : g = 0

Goal state after:
case pos
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : g = 0
⊢ (f * g).reverse = f.reverse * g.reverse

case neg
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : ¬g = 0
⊢ (f * g).reverse = f.reverse * g.reverse
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case none
ι : Type w
S : Type u_1
inst✝ : Semiring S
f : ι → S[X]
s : Finset ι
hf : ∑ k ∈ s, (f k).leadingCoeff ≠ 0
hd : ∀ k ∈ s, (f k).degree = none
⊢ (∑ k ∈ s, f k).leadingCoeff = ∑ k ∈ s, (f k).leadingCoeff

Tactic:
simp_all [WithBot.none_eq_bot]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) ↔
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)

Tactic:
constructor <;> intro h f g hf hg he

Goal state after:
case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
f g : R[X]
hf : f.Monic
hg : g.Monic
he : f * g = p
⊢ ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)

case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
f g : R[X]
hf : f.Monic
hg : g.Monic
he : f * g = p
⊢ f.natDegree = 0 ∨ g.natDegree = 0