mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ IsPretransitive G α ↔ Subsingleton (orbitRel.Quotient G α)

Tactic:
refine ⟨fun _ ↦ ⟨fun a b ↦ ?_⟩, fun _ ↦ ⟨fun a b ↦ ?_⟩⟩
  · refine Quot.inductionOn a (fun x ↦ ?_)
    exact Quot.inductionOn b (fun y ↦ Quot.sound <| exists_smul_eq G y x)
  · have h : Quotient.mk (orbitRel G α) b = ⟦a⟧ := Subsingleton.elim _ _
    exact Quotient.eq''.mp h

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

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : k ≠ 0
⊢ p.minFac = p

Tactic:
hp.minFac_eq

Goal state after:
p k : ℕ
hp : Prime p
hk : k ≠ 0
⊢ p = p
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.cons.zero
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hn : (a :: l).rotate 0 = b :: m
⊢ IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])

Tactic:
simp only [rotate_zero, cons.injEq] at hn

Goal state after:
case cons.cons.zero
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hn : a = b ∧ l = m
⊢ IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
Module: Mathlib.Data.List.Prime

Goal state before:
pp: case mp.cons
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ (L_hd :: L_tl).prod
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a

Tactic:
rw [prod_cons] at h
      rcases pp.dvd_or_dvd h with hd | hd
      · exact ⟨L_hd, mem_cons_self, hd⟩
      · obtain ⟨x, hx1, hx2⟩ := L_ih hd
        exact ⟨x, mem_cons_of_mem L_hd hx1, hx2⟩

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
⊢ a ∉ H

Tactic:
rw [← inv_mem_iff (x := a), ← ha, inv_mul_cancel]

Goal state after:
case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
⊢ 1 ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : Surjective ⇑f
⊢ (H ⊔ f.ker).index * f.range.index ∣ H.index

Tactic:
f.range_eq_top_of_surjective hf,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : Surjective ⇑f
⊢ (H ⊔ f.ker).index * ⊤.index ∣ H.index
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
J K : Subgroup G'
hJK : J.relIndex K ≠ 0
⊢ (comap f J).relIndex (comap f K) ≠ 0

Tactic:
relIndex_comap

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
J K : Subgroup G'
hJK : J.relIndex K ≠ 0
⊢ J.relIndex (map f (comap f K)) ≠ 0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬H.relIndex L = 0
⊢ H.relIndex (K ⊓ L) * K.relIndex L ≤ H.relIndex L * K.relIndex L

Tactic:
relIndex_le_of_le_right inf_le_right h

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬H.relIndex L = 0
⊢ H.relIndex L * K.relIndex L ≤ H.relIndex L * K.relIndex L
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L

Tactic:
by
  by_cases h : H.relIndex L = 0
  · simp [relIndex_eq_zero_of_le_left inf_le_left h]
  rw [← inf_relIndex_right, inf_assoc, ← relIndex_mul_relIndex _ _ L inf_le_right inf_le_right,
    inf_relIndex_right, inf_relIndex_right]
  grw [relIndex_le_of_le_right inf_le_right h]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (H ⊓ K).index ≤ H.index * K.index

Tactic:
by
  simp_rw [← relIndex_top_right, relIndex_inf_le]

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
k : ℤ
⊢ ↑n ∣ k → ↑k = 0

Tactic:
CharP.intCast_eq_zero_iff (ZMod n) n

Goal state after:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
k : ℤ
⊢ ↑n ∣ k → ↑n ∣ k
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
H K L : Subgroup G
f : G →* G'
inst✝ : H.FiniteIndex
⊢ H.normalCore.FiniteIndex

Tactic:
rw [normalCore_eq_ker]
  infer_instance

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
a b : ℕ
hab : a < b
ha : a * (n / a) = n
hb : b * (n / b) = n
⊢ n / b < n / a

Tactic:
rwa [Nat.div_lt_div_left hn ⟨_, hb.symm⟩ ⟨_, ha.symm⟩]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
a✝ : ℕ
⊢ a✝ = 1 ∨ a✝ = p ↔ a✝ = 1 ∨ a✝ ∈ {p}

Tactic:
Finset.mem_singleton

Goal state after:
p : ℕ
pp : Prime p
a✝ : ℕ
⊢ a✝ = 1 ∨ a✝ = p ↔ a✝ = 1 ∨ a✝ = p
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x
⊢ s = (n✝ + 1).properDivisors

Tactic:
apply Subset.antisymm hsub

Goal state after:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x
⊢ (n✝ + 1).properDivisors ⊆ s
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
hn : Odd n
a : ZMod n
⊢ a + a = 0 ↔ a = 0

Tactic:
by
  rw [Nat.odd_iff, ← Nat.two_dvd_ne_zero, ← Nat.prime_two.coprime_iff_not_dvd] at hn
  rw [← mul_two, ← @Nat.cast_two (ZMod n), ← ZMod.coe_unitOfCoprime 2 hn, Units.mul_left_eq_zero]

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ (↑n * m).natAbs

Tactic:
Int.natAbs_mul,

Goal state after:
case inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ (↑n).natAbs * m.natAbs
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case case3
n p p✝ : ℕ
hp✝ : 1 < p✝ ∧ n ≠ 0
h✝ : ¬n % p✝ = 0
⊢ (0, n).snd * p✝ ^ (0, n).fst = n ∧ ¬p✝ ∣ (0, n).snd

Tactic:
| case3 =>

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

Goal state before:
pp: case succ.succ
n p : ℕ
a✝¹ : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
a✝ : ((p + 1).digits n).sum ≤ n
⊢ ((p + 1).digits (n + 1)).sum ≤ n + 1

Tactic:
nth_rw 2 [← ofDigits_digits p.succ (n + 1)]

Goal state after:
case succ.succ
n p : ℕ
a✝¹ : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
a✝ : ((p + 1).digits n).sum ≤ n
⊢ ((p + 1).digits (n + 1)).sum ≤ ofDigits p.succ (p.succ.digits (n + 1))
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inl
p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < p
h : 1 < p
⊢ (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum

pp: case inr.inl
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < 1
⊢ (1 - 1) * ∑ i ∈ range L.length, ofDigits 1 L / 1 ^ i.succ = ofDigits 1 L - L.sum

pp: case inr.inr
p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < p
h : p < 1
⊢ (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum

Tactic:
· induction L with
    | nil => simp [ofDigits]
    | cons hd tl ih =>
      simp only [List.length_cons, List.sum_cons, self_div_pow_eq_ofDigits_drop _ _ h,
          digits_ofDigits p h (hd :: tl) h_lt (fun _ => h_ne_zero)]
      simp only [ofDigits]
      rw [sum_range_succ, Nat.cast_id]
      simp only [List.drop, List.drop_length]
      obtain rfl | h' := em <| tl = []
      · simp [ofDigits]
      · have w₁' := fun l hl ↦ h_lt l <| List.mem_cons_of_mem hd hl
        have w₂' := fun (h : tl ≠ []) ↦ (List.getLast_cons h) ▸ h_ne_zero
        have ih := ih (w₂' h') w₁'
        simp only [self_div_pow_eq_ofDigits_drop _ _ h, digits_ofDigits p h tl w₁' w₂',
          ← Nat.one_add] at ih
        have := sum_singleton (fun x ↦ ofDigits p <| tl.drop x) tl.length
        rw [← Ico_succ_singleton, List.drop_length, ofDigits] at this
        have h₁ : 1 ≤ tl.length := List.length_pos_iff.mpr h'
        rw [← sum_range_add_sum_Ico _ <| h₁, ← add_zero (∑ x ∈ Ico _ _, ofDigits p (tl.drop x)),
            ← this, sum_Ico_consecutive _ h₁ <| (le_add_right tl.length 1),
            ← sum_Ico_add _ 0 tl.length 1,
            Ico_zero_eq_range, mul_add, mul_add, ih, range_one, sum_singleton, List.drop, ofDigits,
            mul_zero, add_zero, ← Nat.add_sub_assoc <| sum_le_ofDigits _ <| Nat.le_of_lt h]
        nth_rw 2 [← one_mul <| ofDigits p tl]
        rw [← add_mul, Nat.sub_add_cancel (one_le_of_lt h), Nat.add_sub_add_left]

Goal state after:
case inr.inl
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < 1
⊢ (1 - 1) * ∑ i ∈ range L.length, ofDigits 1 L / 1 ^ i.succ = ofDigits 1 L - L.sum

case inr.inr
p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < p
h : p < 1
⊢ (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: p i n : ℕ
h : 2 ≤ p
⊢ n % p ^ i = ofDigits p (List.take i (p.digits n))

Tactic:
convert!
    ofDigits_mod_pow_eq_ofDigits_take i (zero_lt_of_lt h) (p.digits n)
      (fun l hl ↦ digits_lt_base h hl)
  exact (ofDigits_digits p n).symm

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: a b n : ℕ
ha : Nat.Prime a
hb : b ≠ 0
⊢ n ≤ padicValNat a b ↔ ↑n ≤ ↑(padicValNat a b)

Tactic:
Nat.cast_le

Goal state after:
a b n : ℕ
ha : Nat.Prime a
hb : b ≠ 0
⊢ n ≤ padicValNat a b ↔ n ≤ padicValNat a b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

Tactic:
rw [emultiplicity_add_of_gt hab, min_eq_right]
    exact le_of_lt hab

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ orderOf (x ^ n) ∣ orderOf x

Tactic:
by
  rw [orderOf_dvd_iff_pow_eq_one, pow_right_comm, pow_orderOf_eq_one, one_pow]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
⊢ multiplicity p a = 0

Tactic:
by
  apply Nat.eq_zero_of_not_pos
  intro nh
  have da : p ∣ a := by simpa [multiplicity_eq_zero] using nh.ne.symm
  have db : p ∣ b := by simpa [multiplicity_eq_zero] using (nh.trans_le hle).ne.symm
  have := Nat.dvd_gcd da db
  rw [Coprime.gcd_eq_one hab, Nat.dvd_one] at this
  exact hp this

Goal state after:
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
⊢ (n.choose k).factorization p = ((n - k + k).choose k).factorization p

Tactic:
Nat.sub_add_cancel hkn

Goal state after:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
⊢ (n.choose k).factorization p = (n.choose k).factorization p
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ multiplicity p (p ^ n)! = ∑ i ∈ range n, p ^ i

Tactic:
rw [← ENat.natCast_inj, ← (Nat.finiteMultiplicity_iff.2
      ⟨hp.ne_one, (p ^ n).factorial_pos⟩).emultiplicity_eq_multiplicity]

Goal state after:
n p : ℕ
hp : Prime p
⊢ emultiplicity p (p ^ n)! = ↑(∑ i ∈ range n, p ^ i)
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocRing R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Finite R
⊢ p ≠ 0

Tactic:
rintro rfl
  have : CharZero R := charP_to_charZero R
  exact absurd Nat.cast_injective (not_injective_infinite_finite ((↑) : ℕ → R))

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
hx : ¬IsOfFinOrder x
h : zpowers x = zpowers y
hx_mem : x ∈ zpowers y
⊢ x = y ∨ x⁻¹ = y

Tactic:
have hy_mem : y ∈ zpowers x := by simp [h]

Goal state after:
G : Type u_1
inst✝ : Group G
x y : G
hx : ¬IsOfFinOrder x
h : zpowers x = zpowers y
hx_mem : x ∈ zpowers y
hy_mem : y ∈ zpowers x
⊢ x = y ∨ x⁻¹ = y
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
⊢ of' k G g %ᵒᶠ g = 0

Tactic:
by
  simpa only [one_mul] using mul_of'_modOf (1 : k[G]) g

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
⊢ g • a = a

Tactic:
have key := smul_mono_right g (le_pow_smul h (Nat.card G - 1))

Goal state after:
G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
key : g • a ≤ g • g ^ (Nat.card G - 1) • a
⊢ g • a = a
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case refine_2.inl.inr
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
p q : R[X]
hp : p.natDegree = 0
hq : M q
⊢ M (C (p.coeff 0) + q)

Tactic:
exact h_C_add hq

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
⊢ X ^ (n + 1) ∣ f

Tactic:
obtain ⟨g, hgf⟩ := hn fun d : ℕ => fun H : d < n => hd _ (Nat.lt_succ_of_lt H)
      have := coeff_X_pow_mul g n 0
      rw [zero_add, ← hgf, hd n (Nat.lt_succ_self n)] at this
      obtain ⟨k, hgk⟩ := Polynomial.X_dvd_iff.mpr this.symm
      use k
      rwa [pow_succ, mul_assoc, ← hgk]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
ih :
  ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2 =
    p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)
⊢ (have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
      have _wf := ⋯;
      have dm := (p - q * z).divModByMonicAux ⋯;
      (z + dm.1, dm.2)).2 =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0

Tactic:
refine ih.trans ?_

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
ih :
  ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2 =
    p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)
⊢ p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q) =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ C ↑h.unit⁻¹ * -(X - C a) + C ↑h.unit⁻¹ * (X - C b) = 1

Tactic:
← left_distrib,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ C ↑h.unit⁻¹ * (-(X - C a) + (X - C b)) = 1
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ ↑q.natDegree ≤ ↑(q.natDegree + (p /ₘ q).natDegree)

Tactic:
Nat.cast_le

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ q.natDegree ≤ q.natDegree + (p /ₘ q).natDegree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ((map f p).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) = map f (∑ a ∈ range (n + 1), C (p.coeff a * ↑a) * X ^ (a - 1))

pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0

Tactic:
on_goal 1 => rw [sum_over_range' _ _ (n + 1) ((le_max_right _ _).trans_lt (lt_add_one _))]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ∑ a ∈ range (n + 1), C ((map f p).coeff a * ↑a) * X ^ (a - 1) =
    map f (∑ a ∈ range (n + 1), C (p.coeff a * ↑a) * X ^ (a - 1))

R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0

R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ derivative (∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)) =
    ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k + 1] p * (⇑derivative)^[k] q) +
      ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q)

Tactic:
simp only [Nat.succ_eq_add_one, nsmul_eq_mul, derivative_mul, derivative_natCast, zero_mul,
          derivative_sum, zero_add, Function.iterate_succ', Function.comp_apply]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ x ∈ range (n + 1),
      ↑(n.choose x) *
        (derivative ((⇑derivative)^[n - x] p) * (⇑derivative)^[x] q +
          (⇑derivative)^[n - x] p * derivative ((⇑derivative)^[x] q)) =
    ∑ x ∈ range (n + 1), ↑(n.choose x) * (derivative ((⇑derivative)^[n - x] p) * (⇑derivative)^[x] q) +
      ∑ x ∈ range (n + 1), ↑(n.choose x) * ((⇑derivative)^[n - x] p * derivative ((⇑derivative)^[x] q))
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr.refine_1.e_a.refine_2
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ a ^ (i - (n + 1 + 1) + 1) * p.coeff i = a ^ (i - (n + 1)) * p.coeff i

Tactic:
i.sub_succ',

Goal state after:
case inr.refine_1.e_a.refine_2
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ a ^ (i - (n + 1) - 1 + 1) * p.coeff i = a ^ (i - (n + 1)) * p.coeff i
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p /ₘ q).leadingCoeff = (q * (p /ₘ q)).leadingCoeff

pp: R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p %ₘ q).degree < (q * (p /ₘ q)).degree

Tactic:
leadingCoeff_monic_mul hmonic

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p /ₘ q).leadingCoeff = (p /ₘ q).leadingCoeff

R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p %ₘ q).degree < (q * (p /ₘ q)).degree
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
h : WellFoundedLT (Associates α)
⊢ WellFounded DvdNotUnit

Tactic:
convert h.wf

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
h : WellFoundedLT (Associates α)
x✝¹ x✝ : Associates α
⊢ DvdNotUnit x✝¹ x✝ ↔ x✝¹ < x✝
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case succ
α : Type u_5
s : Set α
n : ℕ
ih : n • (fun x ↦ single x 1) '' s = {x | degree x = n ∧ ↑x.support ⊆ s}
⊢ {x | degree x = n ∧ ↑x.support ⊆ s} + (fun x ↦ single x 1) '' s = {x | degree x = n + 1 ∧ ↑x.support ⊆ s}

Tactic:
refine subset_antisymm ?_ fun f ⟨f_deg, f_supp⟩ ↦ ?_

Goal state after:
case succ.refine_1
α : Type u_5
s : Set α
n : ℕ
ih : n • (fun x ↦ single x 1) '' s = {x | degree x = n ∧ ↑x.support ⊆ s}
⊢ {x | degree x = n ∧ ↑x.support ⊆ s} + (fun x ↦ single x 1) '' s ⊆ {x | degree x = n + 1 ∧ ↑x.support ⊆ s}

case succ.refine_2
α : Type u_5
s : Set α
n : ℕ
ih : n • (fun x ↦ single x 1) '' s = {x | degree x = n ∧ ↑x.support ⊆ s}
f : α →₀ ℕ
x✝ : f ∈ {x | degree x = n + 1 ∧ ↑x.support ⊆ s}
f_deg : degree f = n + 1
f_supp : ↑f.support ⊆ s
⊢ f ∈ {x | degree x = n ∧ ↑x.support ⊆ s} + (fun x ↦ single x 1) '' s
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case cons.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ia : Irreducible a
ih : (∀ a ∈ 0, Irreducible a) → normalizedFactors (Multiset.prod 0) = Multiset.map normalize 0
hs : ∀ a_1 ∈ a ::ₘ 0, Irreducible a_1
ib : ∀ b ∈ 0, Irreducible b
⊢ normalizedFactors a = Multiset.map normalize {a}

Tactic:
Multiset.map_singleton,

Goal state after:
case cons.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ia : Irreducible a
ih : (∀ a ∈ 0, Irreducible a) → normalizedFactors (Multiset.prod 0) = Multiset.map normalize 0
hs : ∀ a_1 ∈ a ::ₘ 0, Irreducible a_1
ib : ∀ b ∈ 0, Irreducible b
⊢ normalizedFactors a = {normalize a}
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:

Tactic:
Multiset.prod (p ::ₘ fx) ~ᵤ a * b := by
              rw [hx, Multiset.prod_cons]; exact hfx.2.mul_left _
            _ ~ᵤ fa.prod * fb.prod := hfa.2.symm.mul_mul hfb.2.symm
            _ = _ := by rw [Multiset.prod_add]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
x✝ : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
⊢ p * b ~ᵤ (p ::ₘ factors b).prod

Tactic:
rw [prod_cons]; exact (factors_prod hb0).symm.mul_left _

Goal state after: