mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
M0 : Submodule R M
ih :
  ∀ N' ≤ M0,
    ∀ x ∈ M0,
      (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) →
        ∀ N ≤ N', ∃ n o, ∃ (hno : n ≤ o), ∃ bO bN a, ∀ (i : Fin n), ↑(bN i) = a i • ↑(bO (Fin.castLE hno i))
N : Submodule R M
N_le_O : N ≤ M0
m : ℕ
b'M : Basis (Fin m) R ↥M0
N_bot : ¬N = ⊥
y : M
hy : y ∈ M0
a : R
left✝² : a • y ∈ N
M' : Submodule R M
M'_le_M : M' ≤ M0
N' : Submodule R M
left✝¹ : N' ≤ N
N'_le_M' : N' ≤ M'
y_ortho : ∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0
left✝ : ∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0
h :
  ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'),
    ∃ bN,
      ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'),
        ∃ (hnm : n' + 1 ≤ m' + 1),
          ∃ bM,
            ∀ (as : Fin n' → R),
              (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) →
                ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
n' m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis (Fin m') R ↥M'
bN' : Basis (Fin n') R ↥N'
as' : Fin n' → R
has' : ∀ (i : Fin n'), ↑(bN' i) = as' i • ↑(bM' (Fin.castLE hn'm' i))
bN : Basis (Fin (n' + 1)) R ↥N
h' :
  ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'),
    ∃ (hnm : n' + 1 ≤ m' + 1),
      ∃ bM,
        ∀ (as : Fin n' → R),
          (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) →
            ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
hmn : n' + 1 ≤ m' + 1
bM : Basis (Fin (m' + 1)) R ↥M0
h'' :
  ∀ (as : Fin n' → R),
    (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) →
      ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hmn i))
as : Fin (n' + 1) → R
has : ∀ (i : Fin (n' + 1)), ↑(bN i) = as i • ↑(bM (Fin.castLE hmn i))
⊢ ∃ n o, ∃ (hno : n ≤ o), ∃ bO bN a, ∀ (i : Fin n), ↑(bN i) = a i • ↑(bO (Fin.castLE hno i))

Tactic:
exact ⟨_, _, hmn, bM, bN, as, has⟩

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
b✝ : ι → M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
b : Basis ι R M
N O : Submodule R M
N_le_O : N ≤ O
⊢ (o : ℕ) × (n : ℕ) × Basis.SmithNormalForm (comap O.subtype N) (Fin o) n

Tactic:
choose n o hno bO bN a snf using N.exists_smith_normal_form_of_le b O N_le_O
  refine
    ⟨o, n, bO, bN.map (comapSubtypeEquivOfLe N_le_O).symm, (Fin.castLEEmb hno), a,
      fun i ↦ ?_⟩
  ext
  simp only [snf, Basis.map_apply, Submodule.comapSubtypeEquivOfLe_symm_apply,
    Submodule.coe_smul_of_tower, Fin.castLEEmb_apply]

Goal state after:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
f1 f2 : K →+* L
hf : ∀ (x : A), f1 ((algebraMap A K) x) = f2 ((algebraMap A K) x)
⊢ f1 = f2

Tactic:
ext z
  obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective A z
  rw [map_div₀, map_div₀, hf, hf]

Goal state after:
Module: Mathlib.Algebra.Star.StarProjection

Goal state before:
pp: R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ (p * q = p ∧ q * p = p) ∧ IsSelfAdjoint (q - p) ↔ p * q = p

Tactic:
simp_rw [hq.isSelfAdjoint.sub hp.isSelfAdjoint, and_true]

Goal state after:
R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ p * q = p ∧ q * p = p ↔ p * q = p
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: case e'_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : (PreQuasiregular A)ˣ
⊢ (1 + ↑(PreQuasiregular.equiv.symm ↑x)) * (1 + ↑(PreQuasiregular.equiv.symm ↑x⁻¹)) =
    1 + ↑((↑x⁻¹).val + (↑x).val + (↑x).val * (↑x⁻¹).val)

Tactic:
simp only [mul_one, PreQuasiregular.equiv_symm_apply, one_mul, mul_add,
              add_mul, inr_add, inr_mul]

Goal state after:
case e'_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : (PreQuasiregular A)ˣ
⊢ 1 + ↑(↑x).val + (↑(↑x⁻¹).val + ↑(↑x).val * ↑(↑x⁻¹).val) = 1 + (↑(↑x⁻¹).val + ↑(↑x).val + ↑(↑x).val * ↑(↑x⁻¹).val)
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: case e'_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : (PreQuasiregular A)ˣ
⊢ (1 + ↑(PreQuasiregular.equiv.symm ↑x⁻¹)) * (1 + ↑(PreQuasiregular.equiv.symm ↑x)) =
    1 + ↑((↑x).val + (↑x⁻¹).val + (↑x⁻¹).val * (↑x).val)

Tactic:
simp only [mul_one, PreQuasiregular.equiv_symm_apply, one_mul, mul_add,
              add_mul, inr_add, inr_mul]

Goal state after:
case e'_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : (PreQuasiregular A)ˣ
⊢ 1 + ↑(↑x⁻¹).val + (↑(↑x).val + ↑(↑x⁻¹).val * ↑(↑x).val) = 1 + (↑(↑x).val + ↑(↑x⁻¹).val + ↑(↑x⁻¹).val * ↑(↑x).val)
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : A
hx : IsUnit (1 + ↑x)
⊢ IsQuasiregular x

Tactic:
exact ⟨(Unitization.unitsFstOne_mulEquiv_quasiregular R) ⟨hx.unit, by simp⟩, by simp⟩

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

Goal state before:
pp: case mem
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r✝ : R
a : A
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
r : R
hr : r ∈ range fun s ↦ star s * s
⊢ r • a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)

Tactic:
| mem r hr =>

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

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ ∀ x ∈ range fun s ↦ star s * s, ∀ (x_1 y : R), y = x_1 + x → x_1 ≤ y

pp: case refine_2.refine_2
R : Type u_1
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ ∀ (x y : R),
    x ∈ AddSubmonoid.closure (range fun s ↦ star s * s) →
      y ∈ AddSubmonoid.closure (range fun s ↦ star s * s) →
        (∀ (x_1 y : R), y = x_1 + x → x_1 ≤ y) →
          (∀ (x y_1 : R), y_1 = x + y → x ≤ y_1) → ∀ (x_1 y_1 : R), y_1 = x_1 + (x + y) → x_1 ≤ y_1

Tactic:
· rintro _ ⟨s, rfl⟩ x y rfl
        exact (h_le_iff _ _).mpr ⟨s, rfl⟩

Goal state after:
case refine_2.refine_2
R : Type u_1
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ ∀ (x y : R),
    x ∈ AddSubmonoid.closure (range fun s ↦ star s * s) →
      y ∈ AddSubmonoid.closure (range fun s ↦ star s * s) →
        (∀ (x_1 y : R), y = x_1 + x → x_1 ≤ y) →
          (∀ (x y_1 : R), y_1 = x + y → x ≤ y_1) → ∀ (x_1 y_1 : R), y_1 = x_1 + (x + y) → x_1 ≤ y_1
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ x ∈ t.erase x₀, g (x - x₀) • (x - x₀) = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
x : M
x_mem : x ∈ t.erase x₀
⊢ (if x = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (x - x₀)) • x - g (x - x₀) • x₀ =
    g (x - x₀) • x - g (x - x₀) • x₀

Tactic:
rw [if_neg (mem_erase.mp x_mem).1]

Goal state after:
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
v : V
hfv : f v ≠ 0
b₁ : Basis (↑(Basis.ofVectorSpaceIndex K ↥f.ker)) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
i : ↑n := ⟨v, ⋯⟩
⊢ ∃ n b i, v = b i ∧ f = f v • b.coord i

Tactic:
have hi : b i = v := by simp [b, i]

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
v : V
hfv : f v ≠ 0
b₁ : Basis (↑(Basis.ofVectorSpaceIndex K ↥f.ker)) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
i : ↑n := ⟨v, ⋯⟩
hi : b i = v
⊢ ∃ n b i, v = b i ∧ f = f v • b.coord i
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case refine_1
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this : Nontrivial K
h : Module.rank K V = 1
v₀ : V
hzero : v₀ = 0
hv : ∀ (v : V), ∃ r, r • 0 = v
⊢ False

Tactic:
smul_zero,

Goal state after:
case refine_1
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this : Nontrivial K
h : Module.rank K V = 1
v₀ : V
hzero : v₀ = 0
hv : ∀ (v : V), ∃ r, 0 = v
⊢ False
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ (k + m))

Tactic:
add_comm m 1,

Goal state after:
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ (k + (1 + m))) ≤ LinearMap.ker (f ^ (k + m))
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case h'
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f : E →ₛₗ.[σ] F
x : E
y : x ∈ (- -f).domain
hxy : x ∈ f.domain
⊢ ↑(- -f) ⟨x, y⟩ = ↑f ⟨x, hxy⟩

Tactic:
· simp only [neg_apply, neg_neg]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.comp (C 0) = C (eval 0 p)

Tactic:
comp_C

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ C (eval 0 p) = C (eval 0 p)
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.comp (C 1) = C (eval 1 p)

Tactic:
comp_C

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ C (eval 1 p) = C (eval 1 p)
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: p : ℕ
⊢ Prime p ↔ 2 ≤ p ∧ ¬∃ m n, m < p ∧ n < p ∧ m * n = p

Tactic:
by
  push Not
  simp_rw [prime_def_lt, dvd_def, exists_imp]
  refine and_congr_right fun hp ↦ forall_congr' fun m ↦ (forall_congr' fun h ↦ ?_).trans forall_comm
  simp_rw [Ne, forall_comm (β := _ = _), eq_comm, imp_false, not_lt]
  refine forall₂_congr fun n hp ↦ ⟨by simp_all, fun hpn ↦ ?_⟩
  have := mul_ne_zero_iff.mp (hp ▸ show p ≠ 0 by lia)
  exact (Nat.mul_eq_right (by lia)).mp
    (hp.symm.trans (hpn.antisymm (hp ▸ Nat.le_mul_of_pos_left _ (by lia))))

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

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

Tactic:
intro h
    rw [← h]
    exact minFac_dvd n

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Mul M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : M →ₙ* A
a₁ a₂ : R[M]
⊢ (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom)).toFun (a₁ * a₂) =
    (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom)).toFun a₁ *
      (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom)).toFun a₂

Tactic:
by
      simpa [mul_def, sum_sum_index, add_smul, Finsupp.mul_sum, Finsupp.sum_mul,
        smul_mul_smul_comm] using Finsupp.sum_comm ..

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

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
F : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
r : R
⊢ mapDomain (⇑f) ((algebraMap R A[M]) r) = (algebraMap R A[N]) r

Tactic:
simp only [coe_algebraMap, mapDomain_single, map_one, (· ∘ ·)]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Add M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : Multiplicative M →ₙ* A
a₁ a₂ : R[M]
⊢ (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp coeffAddEquiv.toAddMonoidHom)).toFun
      (a₁ * a₂) =
    (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp coeffAddEquiv.toAddMonoidHom)).toFun
        a₁ *
      (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp
              coeffAddEquiv.toAddMonoidHom)).toFun
        a₂

Tactic:
by
      simpa [mul_def, sum_sum_index, add_smul, Finsupp.mul_sum, Finsupp.sum_mul,
        smul_mul_smul_comm] using Finsupp.sum_comm ..

Goal state after:
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
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
⊢ Monic D 1

Tactic:
by
  rw [Monic, one_def, leadingCoeff_single hD]

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]
h₁ : p ∣ q
h₂ : q.degree < p.degree
⊢ q = 0

Tactic:
by_contra hc

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h₁ : p ∣ q
h₂ : q.degree < p.degree
hc : ¬q = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h₁ : p ∣ q
h₂ : q.natDegree < p.natDegree
⊢ q = 0

Tactic:
by_contra hc

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h₁ : p ∣ q
h₂ : q.natDegree < p.natDegree
hc : ¬q = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn : p ^ n ≠ 0
⊢ ↑(p ^ n).natDegree = ↑(n * p.natDegree)

Tactic:
rw [← degree_eq_natDegree hpn, degree_pow' h, degree_eq_natDegree hp0]; simp

Goal state after:
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
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hbot : ⊥ + ⊥ = ⊥
hp : Monic D p
hq : Monic D q
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
by
  cases subsingleton_or_nontrivial R
  · simp_rw [Subsingleton.eq_zero p, Subsingleton.eq_zero q, mul_zero, supDegree_zero, hbot]
  exact hq.supDegree_mul_of_ne_zero_left hD hadd hp.ne_zero

Goal state after:
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]
n : ℕ
hn : p.natDegree < n
x : S
⊢ eval₂ f x p = ∑ i ∈ range n, f (p.coeff i) * x ^ i

Tactic:
by
  rw [eval₂_eq_sum, p.sum_over_range' _ _ hn]
  intro i
  rw [f.map_zero, zero_mul]

Goal state after:
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 : f (p.coeff p.natDegree) = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ p = 0

Tactic:
← coeff_map,

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).coeff p.natDegree = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ p = 0
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝¹ : Zero α
inst✝ : Preorder α
i : ι
a b : α
⊢ single i a ≤ single i b ↔ a ≤ b

Tactic:
exact Pi.single_le_single

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝¹ : LinearOrder ι
x y : (i : ι) → β i
i : ι
inst✝ : (i : ι) → LinearOrder (β i)
h : ∀ (j : ι), j < i → x j = y j
hxy : y i < x i
⊢ toLex y < toLex x

Tactic:
use i

Goal state after:
case h
ι : Type u_1
β : ι → Type u_2
inst✝¹ : LinearOrder ι
x y : (i : ι) → β i
i : ι
inst✝ : (i : ι) → LinearOrder (β i)
h : ∀ (j : ι), j < i → x j = y j
hxy : y i < x i
⊢ (∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j i → toLex y j = toLex x j) ∧ (fun {i} x1 x2 ↦ x1 < x2) (toLex y i) (toLex x i)
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝¹ : LinearOrder ι
x y : (i : ι) → β i
i : ι
inst✝ : (i : ι) → LinearOrder (β i)
h : ∀ (j : ι), j > i → x j = y j
hxy : y i < x i
⊢ toColex y < toColex x

Tactic:
use i

Goal state after:
case h
ι : Type u_1
β : ι → Type u_2
inst✝¹ : LinearOrder ι
x y : (i : ι) → β i
i : ι
inst✝ : (i : ι) → LinearOrder (β i)
h : ∀ (j : ι), j > i → x j = y j
hxy : y i < x i
⊢ (∀ (j : ι), (fun x1 x2 ↦ x1 > x2) j i → toColex y j = toColex x j) ∧
    (fun {i} x1 x2 ↦ x1 < x2) (toColex y i) (toColex x i)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
a : R
e : ℕ
n : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (monomial (s + Finsupp.single n e)) a = (monomial s) a * X n ^ e

Tactic:
rw [X_pow_eq_monomial, monomial_mul, mul_one]

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 = C 1 * (Finsupp.indicator t fun i x_1 ↦ x i).prod fun n e ↦ X n ^ e

Tactic:
C_1,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → ℕ
t : Finset σ
⊢ ∏ y ∈ t, X y ^ x y = 1 * (Finsupp.indicator t fun i x_1 ↦ x i).prod fun n e ↦ X n ^ e
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : ℕ
⊢ eval₂ f g (p ^ (n + 1)) = eval₂ f g p ^ (n + 1)

Tactic:
rw [pow_add, pow_one, pow_add, pow_one, eval₂_mul, eval₂_pow]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
this : coeff m (C 1 * (Finsupp.single i k).prod fun n e ↦ X n ^ e) = if Finsupp.single i k = m then 1 else 0
⊢ coeff m (X i ^ k) = if Finsupp.single i k = m then 1 else 0

Tactic:
C_1,

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
this : coeff m (1 * (Finsupp.single i k).prod fun n e ↦ X n ^ e) = if Finsupp.single i k = m then 1 else 0
⊢ coeff m (X i ^ k) = if Finsupp.single i k = m then 1 else 0
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
i : σ
⊢ (killCompl hf) ((rename f) (X i)) = X i

Tactic:
rw [rename_X, killCompl, aeval_X, dif_pos ⟨i, rfl⟩, Equiv.ofInjective_symm_apply]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ (∏ i ∈ s, f i).degrees ≤ ∑ i ∈ s, (f i).degrees

Tactic:
classical exact supDegree_prod_le (map_zero _) (map_add _)

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ constantCoeff.comp C = RingHom.id R

Tactic:
by
  ext x
  exact constantCoeff_C σ x

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

Goal state before:
pp: case refine_1
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : ∀ (a : σ), a ∉ p.degrees
s : σ →₀ ℕ
hs : s ∈ p.support
⊢ s = 0

Tactic:
← Finsupp.support_eq_empty

Goal state after:
case refine_1
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : ∀ (a : σ), a ∉ p.degrees
s : σ →₀ ℕ
hs : s ∈ p.support
⊢ s.support = ∅
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ coeffsIn σ (M * N) = coeffsIn σ M * coeffsIn σ N

Tactic:
refine le_antisymm (coeffsIn_le.2 ?_) ?_

Goal state after:
case refine_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ ∀ m ∈ M * N, ∀ (i : σ →₀ ℕ), (monomial i) m ∈ coeffsIn σ M * coeffsIn σ N

case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ coeffsIn σ M * coeffsIn σ N ≤ coeffsIn σ (M * N)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
a : σ →₀ ℕ
s : S₁
p : MvPolynomial σ S₁
ha : a ∉ p.coeff.support
hs : s ≠ 0
hp : ↑p.coeffs ⊆ range ⇑f → p ∈ range ⇑(map f)
ih : ↑((monomial a) s).coeffs ⊆ range ⇑f → (monomial a) s ∈ range ⇑(map f)
hx : ↑((monomial a) s).coeffs ⊆ range ⇑f ∧ ↑p.coeffs ⊆ range ⇑f
q : MvPolynomial σ R
hq : (map f) q = (monomial a) s
u : MvPolynomial σ R
hu : (map f) u = p
⊢ (map f) (q + u) = (monomial a) s + p

Tactic:
simp [hq, hu]

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

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

Tactic:
simp only [degreeOf_eq_sup i, support_mul_X, Finset.sup_map]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ f.support.sup ((fun m ↦ m i) ∘ ⇑(addRightEmbedding (Finsupp.single j 1))) = f.support.sup fun m ↦ m i
Module: Mathlib.Algebra.MvPolynomial.CommRing

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

Tactic:
simp [vars, degrees_neg]

Goal state after: