mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case h
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
m : ℕ
hm : |ArchimedeanOrder.val (ArchimedeanOrder.of x₂)| ≤ m • |ArchimedeanOrder.val (ArchimedeanOrder.of x₁)|
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y₂)| ≤ n • |ArchimedeanOrder.val (ArchimedeanOrder.of y₁)|
⊢ |ArchimedeanOrder.val (ArchimedeanOrder.of (x₂ * y₂))| ≤
    (m * n) • |ArchimedeanOrder.val (ArchimedeanOrder.of (x₁ * y₁))|

Tactic:
convert mul_le_mul hm hn (abs_nonneg _) (nsmul_nonneg (abs_nonneg _) _) <;>
    simp_rw [ArchimedeanOrder.val_of, abs_mul]

Goal state after:
case e'_4
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
m : ℕ
hm : |ArchimedeanOrder.val (ArchimedeanOrder.of x₂)| ≤ m • |ArchimedeanOrder.val (ArchimedeanOrder.of x₁)|
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y₂)| ≤ n • |ArchimedeanOrder.val (ArchimedeanOrder.of y₁)|
⊢ (m * n) • (|x₁| * |y₁|) = m • |x₁| * n • |y₁|
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: case neg
R : Type u_1
inst✝² : LinearOrder R
α : Type u_2
β : Type u_3
inst✝¹ : AddCommMonoid α
inst✝ : Nonempty β
f : α → R
hna : IsNonarchimedean f
g : β → α
a : β
s : Multiset β
h : s ≠ 0 → ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)
hs : a ::ₘ s ≠ 0
h1 : ¬s = 0
⊢ f (g a + (Multiset.map g s).sum) ≤ f (g a) ∨ ∃ a_1 ∈ s, f (g a + (Multiset.map g s).sum) ≤ f (g a_1)

Tactic:
· obtain ⟨w, h2, h3⟩ := h h1
      rcases le_max_iff.mp <| hna (g a) (Multiset.map g s).sum with h4 | h4
      · exact .inl h4
      · exact .inr ⟨w, h2, le_trans h4 h3⟩

Goal state after:
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
α : Type u_2
β : Type u_3
inst✝¹ : AddCommMonoid α
inst✝ : Nonempty β
f : α → R
hna : IsNonarchimedean f
g : β → α
s : Multiset β
hs : s ≠ 0
⊢ ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)

Tactic:
by
  induction s using Multiset.induction_on with
  | empty => contradiction
  | cons a s h =>
    simp only [Multiset.mem_cons, Multiset.map_cons, Multiset.sum_cons, exists_eq_or_imp]
    by_cases h1 : s = 0
    · simp [h1]
    · obtain ⟨w, h2, h3⟩ := h h1
      rcases le_max_iff.mp <| hna (g a) (Multiset.map g s).sum with h4 | h4
      · exact .inl h4
      · exact .inr ⟨w, h2, le_trans h4 h3⟩

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : x.coeff a = 0
⊢ ∑ x_1 ∈ antidiagonal ⋯ ⋯ (a + b), x.coeff x_1.1 * ((single b) r).coeff x_1.2 = x.coeff a * r

Tactic:
simp only [hx, zero_mul]
    rw [sum_congr _ fun _ _ => rfl, sum_empty]
    ext ⟨a1, a2⟩
    simp only [notMem_empty, not_and, Set.mem_singleton_iff,
      mem_antidiagonal, iff_false]
    rintro h2 rfl h1
    rw [← add_right_cancel h1] at hx
    exact h2 hx

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
⊢ (x * (single b) r).coeff (a + b) = x.coeff a * r

Tactic:
by
  by_cases hr : r = 0
  · simp [hr, coeff_mul]
  simp only [hr, coeff_mul, support_single_of_ne, Ne, not_false_iff]
  by_cases hx : x.coeff a = 0
  · simp only [hx, zero_mul]
    rw [sum_congr _ fun _ _ => rfl, sum_empty]
    ext ⟨a1, a2⟩
    simp only [notMem_empty, not_and, Set.mem_singleton_iff,
      mem_antidiagonal, iff_false]
    rintro h2 rfl h1
    rw [← add_right_cancel h1] at hx
    exact h2 hx
  trans ∑ ij ∈ {(a, b)}, x.coeff ij.fst * (single b r).coeff ij.snd
  · apply sum_congr _ fun _ _ => rfl
    ext ⟨a1, a2⟩
    simp only [Set.mem_singleton_iff, Prod.mk_inj, mem_antidiagonal, mem_singleton]
    constructor
    · rintro ⟨_, rfl, h1⟩
      exact ⟨add_right_cancel h1, rfl⟩
    · rintro ⟨rfl, rfl⟩
      simp [hx]
  · simp

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
⊢ ((HahnModule.of R).symm (x • (HahnModule.of R) y)).coeff (x.order + y.order) = x.leadingCoeff * y.leadingCoeff

Tactic:
exact HahnModule.coeff_smul_order_add_order x y

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
⊢ P.IsOrdering

Tactic:
have : HasMemOrNegMem P := ⟨by simp [h]⟩

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
this : HasMemOrNegMem P
⊢ P.IsOrdering
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
⊢ {a | y.coeff a ≠ z.coeff a} ⊆ y.support ∪ z.support

Tactic:
by intro; simp; grind

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : ↥(↑f).domain
⊢ (withTopOrderIso M) (ofLex (↑↑f x)).orderTop = ArchimedeanClass.mk ↑x

Tactic:
by
  by_cases hx0 : x = 0
  · simp [hx0]
  have hx0' : x.val ≠ 0 := by simpa using hx0
  -- Pick a representative `x'` from `stratum` with the same class as `x`.
  -- `f.val x'` is a `HahnSeries.single` whose `orderTop` is known
  obtain ⟨⟨x', hx'mem⟩, hx'0⟩ := exists_ne (0 : seed.stratum (.mk x hx0'))
  have heq : ArchimedeanClass.mk x' = .mk x.val := by
    apply seed.archimedeanClassMk_of_mem_stratum hx'mem
    simpa using hx'0
  let x'' : f.val.domain := ⟨x', mem_domain f hx'mem⟩
  have hx''mem : x''.val ∈ seed.stratum (mk x.val hx0') := hx'mem
  have h0 : (seed.coeff (mk x.val hx0')) ⟨x''.val, hx''mem⟩ ≠ 0 := by
    rw [(LinearMap.map_eq_zero_iff _ (seed.strictMono_coeff _).injective).ne]
    unfold x''
    simpa using hx'0
  have heq' : ArchimedeanClass.mk x''.val = .mk x.val := heq
  rw [← orderTop_eq_iff, apply_of_mem_stratum f hx''mem, ofLex_toLex,
    HahnSeries.orderTop_single h0] at heq'
  simp [← heq']

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : ↥(↑f).domain
hx0 : ↑x ≠ 0
⊢ (ofLex (↑↑f x)).orderTop = ↑(FiniteArchimedeanClass.mk (↑x) hx0)

Tactic:
apply_fun FiniteArchimedeanClass.withTopOrderIso M

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : ↥(↑f).domain
hx0 : ↑x ≠ 0
⊢ (withTopOrderIso M) (ofLex (↑↑f x)).orderTop = (withTopOrderIso M) ↑(FiniteArchimedeanClass.mk (↑x) hx0)
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : FiniteResidueField K
hx : 0 ≤ x
y z : FiniteResidueField K
h : y ≤ z
⊢ y * x ≤ z * x

Tactic:
by
    simp_rw [mul_comm _ x]
    exact mul_le_mul_of_nonneg_left' h hx

Goal state after:
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x ≠ 0
⊢ stdPart x⁻¹ = (stdPart x)⁻¹

Tactic:
rw [stdPart_of_mk_ne_zero hx, stdPart_of_mk_ne_zero, inv_zero]
    rwa [mk_inv, neg_ne_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ swap (map C f) = C f

Tactic:
induction f using Polynomial.induction_on' with

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.natDegree = 0 ∧ p.Monic ↔ p = 1

Tactic:
refine ⟨fun ⟨H₁, H₂⟩ ↦ eq_one_of_monic_natDegree_zero H₂ H₁, fun H ↦ ?_⟩

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
H : p = 1
⊢ p.natDegree = 0 ∧ p.Monic
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
⊢ ?m.59 * (algebraMap ℤ K) b = 1

Tactic:
eq_intCast,

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
⊢ ?m.59 * ↑b = 1
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) ev =
    (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa :
  |(algebraMap ℤ K) ev| =
    |(algebraMap ℤ K) b ^ f.natDegree *
        eval ((algebraMap ℤ K) a * (1 / (algebraMap ℤ K) b)) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|

Tactic:
eq_intCast,

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) ev =
    (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa :
  |↑ev| =
    |(algebraMap ℤ K) b ^ f.natDegree *
        eval ((algebraMap ℤ K) a * (1 / (algebraMap ℤ K) b)) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) ev =
    (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa :
  |↑ev| =
    |(algebraMap ℤ K) b ^ f.natDegree *
        eval ((algebraMap ℤ K) a * (1 / (algebraMap ℤ K) b)) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|

Tactic:
eq_intCast,

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) ev =
    (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = |↑b ^ f.natDegree * eval ((algebraMap ℤ K) a * (1 / ↑b)) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) 0 =
    (algebraMap ℤ K) b ^ f.natDegree *
      eval ((algebraMap ℤ K) a * ((algebraMap ℤ K) b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
⊢ eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) = 0

Tactic:
eq_intCast,

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  ↑0 =
    (algebraMap ℤ K) b ^ f.natDegree *
      eval ((algebraMap ℤ K) a * ((algebraMap ℤ K) b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
⊢ eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) = 0
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
h : (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)
hxy : x ≠ y
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun x1 x2 ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup

Tactic:
· simp only [mem_cons, forall_eq_or_imp, pairwise_cons] at h
      have : x ∉ xs := fun hx ↦ hxy (antisymm h.1.1 (h.2.1 x hx))
      rw [if_pos hxy, dedup_cons_of_notMem (a := x) (by simp [*])]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
S : Type u_2
inst✝² : AddCommGroup S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
p q : R[X]
x : S
⊢ p.smeval x + (-q).smeval x = p.smeval x - q.smeval x

Tactic:
smeval_neg,

Goal state after:
R : Type u_1
inst✝³ : Ring R
S : Type u_2
inst✝² : AddCommGroup S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
p q : R[X]
x : S
⊢ p.smeval x + -q.smeval x = p.smeval x - q.smeval x
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: S : Type u_3
inst✝² : NonAssocRing S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
q : ℕ[X]
n : ℕ
⊢ q.smeval (-↑n) = ↑(q.smeval (-↑n))

Tactic:
rw [smeval_eq_sum, smeval_eq_sum]
  simp only [Polynomial.smul_pow, sum_def]
  simp

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
⊢ Irreducible p ↔ p.roots = 0

Tactic:
have hp0 : p ≠ 0 := by rintro rfl; rw [natDegree_zero] at hp2; cases hp2

Goal state after:
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ Irreducible p ↔ p.roots = 0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case refine_2
p : ℤ[X]
hp : #p.support • 1 = 3
key : ∀ k ∈ p.support, p.coeff k ^ 2 = 1
⊢ #p.support = 3

Tactic:
Nat.smul_one_eq_cast

Goal state after:
case refine_2
p : ℤ[X]
hp : ↑(#p.support) = 3
key : ∀ k ∈ p.support, p.coeff k ^ 2 = 1
⊢ #p.support = 3
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k

Tactic:
by
  induction s using Finset.cons_induction with
  | empty => simp
  | cons i s hi ih =>
    rw [Finset.forall_mem_cons] at hg
    rw [Finset.coe_cons, Set.pairwise_insert] at hgg
    obtain ⟨q, r, -, hf⟩ := ih hg.2 hgg.1
    have hjs {j : ι} (hj : j ∈ s) : i ≠ j := fun hij => hi (hij ▸ hj)
    have hc (j : ι) : ∃ a b, j ∈ s → a * g i + b * g j = 1 :=
      if h : j ∈ s ∧ i ≠ j then
        (hgg.2 j h.1 h.2).1.elim fun a h => h.elim fun b h => ⟨a, b, fun _ => h⟩
      else
        ⟨0, 0, fun hj => (h ⟨hj, hjs hj⟩).elim⟩
    choose a b hab using hc
    refine ⟨(q + ∑ j ∈ s, r j * b j %ₘ g i) /ₘ g i + ∑ j ∈ s, (r j * b j /ₘ g i + r j * a j /ₘ g j),
      Function.update (fun j => r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i),
      ?_, hf.trans ?_⟩
    · rw [Finset.forall_mem_cons, Function.update_self]
      refine ⟨degree_modByMonic_lt _ hg.1, fun j hj => ?_⟩
      rw [Function.update_of_ne (hjs hj).symm]
      exact degree_modByMonic_lt _ (hg.2 j hj)
    · rw [Finset.prod_cons, Finset.sum_cons, Function.update_self, Finset.erase_cons, add_mul,
        add_add_add_comm, ← mul_assoc, ← add_mul, add_comm (_ * g i), ← mul_comm (g i),
        modByMonic_add_div, add_mul, add_assoc, add_right_inj, Finset.sum_mul,
        Finset.sum_mul, ← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
      refine Finset.sum_congr rfl fun j hj => ?_
      rw [Function.update_of_ne (hjs hj).symm, Finset.erase_cons_of_ne _ (hjs hj),
        Finset.prod_cons, ← Finset.mul_prod_erase s g hj]
      simp_rw [← mul_assoc, ← add_mul]
      refine congrArg (· * _) ?_
      rw [add_mul, add_mul, ← add_assoc, ← add_assoc, ← add_mul, ← mul_comm (g i),
        modByMonic_add_div, add_assoc, mul_right_comm (_ /ₘ g j),
        ← add_mul, add_comm (_ * g j) (_ %ₘ g j), mul_comm (_ /ₘ g j),
        modByMonic_add_div, mul_assoc, mul_assoc, ← mul_add,
        add_comm, hab j hj, mul_one]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
⊢ ⊥ < (∏ i ∈ s, g i).degree

Tactic:
rw [bot_lt_iff_ne_bot, degree_ne_bot]

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
⊢ ∏ i ∈ s, g i ≠ 0
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
a✝ : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₁ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₂ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
⊢ ⊥ < (g i ^ n i).degree

Tactic:
rw [bot_lt_iff_ne_bot, degree_ne_bot]

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
a✝ : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₁ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₂ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
⊢ g i ^ n i ≠ 0