mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a + b) = emultiplicity p b

Tactic:
by
  have : FiniteMultiplicity p b := finiteMultiplicity_iff_emultiplicity_ne_top.2 (by simp [·] at h)
  rw [this.emultiplicity_eq_multiplicity] at *
  apply emultiplicity_eq_of_dvd_of_not_dvd
  · apply dvd_add
    · apply pow_dvd_of_le_emultiplicity
      exact h.le
    · simp
  · rw [dvd_add_right]
    · apply this.not_pow_dvd_of_multiplicity_lt
      simp
    apply pow_dvd_of_le_emultiplicity
    exact Order.add_one_le_of_lt h

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n r : ℕ
hx : x ^ (2 * r + 1) = 1
h2 : 2 * (r + 1) = 2 * r + 1 + 1
⊢ x ^ (2 * (r + 1)) = x

Tactic:
rw [h2, pow_succ, hx, one_mul]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this✝ : p ∣ a * b
x✝ : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
hpx : ¬p ^ (n - 1 + 1) ∣ x
this : 1 ≤ n + m
⊢ x * b * p = p ^ (n + m - succ 0 + 1) * s * p

Tactic:
tsub_add_cancel_of_le this

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this✝ : p ∣ a * b
x✝ : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
hpx : ¬p ^ (n - 1 + 1) ∣ x
this : 1 ≤ n + m
⊢ x * b * p = p ^ (n + m) * s * p
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
⊢ p ^ (multiplicity p a + multiplicity p b) ∣ a * b

Tactic:
pow_add

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
⊢ p ^ multiplicity p a * p ^ multiplicity p b ∣ a * b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p n : ℕ
hp : Prime p
⊢ (p ^ n).factorization p = n

Tactic:
simp [factorization_pow, Prime.factorization_self hp]

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

Goal state before:
pp: p k n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ p ^ k ∣ n ↔ p ^ k ∣ p ^ n.factorization p

Tactic:
by
  rw [pow_dvd_pow_iff_le_right pp.one_lt, pp.pow_dvd_iff_le_factorization hn]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
h : m + k ≡ m [MOD orderOf x]
hk : x ^ k = 1
⊢ x ^ (m + k) = x ^ m * x ^ k

Tactic:
pow_add

Goal state after:
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
h : m + k ≡ m [MOD orderOf x]
hk : x ^ k = 1
⊢ x ^ m * x ^ k = x ^ m * x ^ k
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hdb
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ((a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2) ∣ b

pp: case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
· exact prod_pow_dvd_of_le_factorization inf_le_right

Goal state after:
case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : IsMulTorsionFree G
g : G
ha : g ≠ 1
⊢ orderOf g ≤ 1

Tactic:
ne_eq,

Goal state after:
case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : IsMulTorsionFree G
g : G
ha : ¬g = 1
⊢ orderOf g ≤ 1
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
hy_mem : y ∈ zpowers x
⊢ x = y ∨ x⁻¹ = y

Tactic:
obtain ⟨k, rfl⟩ := mem_zpowers_iff.mp hy_mem

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ (x %ᵒᶠ g).coeff g' = x.coeff g'

Tactic:
by
  classical exact Finsupp.filter_apply_pos _ _ h

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

Goal state before:
pp: case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
x : k[G]
g' : G
h : ¬∃ d, g' = g + d
⊢ (single g 1 * x %ᵒᶠ g).coeff g' = 0

Tactic:
rw [coeff_modOf_of_not_exists_add _ _ _ h, coeff_single_mul_of_forall_add_ne]

Goal state after:
case inr.h
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
x : k[G]
g' : G
h : ¬∃ d, g' = g + d
⊢ ∀ (d : G), g + d ≠ g'
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case inl
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g d : G
⊢ (single g 1 * (x /ᵒᶠ g)).coeff (g + d) = x.coeff (g + d)

Tactic:
coeff_single_mul_add,

Goal state after:
case inl
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g d : G
⊢ 1 * (x /ᵒᶠ g).coeff d = x.coeff (g + d)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
⊢ ↑n = 0 ↔ p ∣ n

Tactic:
by
    have H : (p : R) = 0 := by rw [← hn, Nat.cast_card_eq_zero]
    constructor
    · intro h
      rw [← Nat.mod_add_div n p, Nat.cast_add, Nat.cast_mul, H, zero_mul, add_zero] at h
      rw [Nat.dvd_iff_mod_eq_zero]
      apply hR _ (Nat.mod_lt _ _) h
      rw [← hn, Fintype.card_pos_iff]
      exact ⟨0⟩
    · rintro ⟨n, rfl⟩
      rw [Nat.cast_mul, H, zero_mul]

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ (X - C a) ^ (rootMultiplicity a p + n) ∣ p * (X - C a) ^ n

Tactic:
pow_add

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ (X - C a) ^ rootMultiplicity a p * (X - C a) ^ n ∣ p * (X - C a) ^ n
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
a : R
p : R[X]
⊢ ((a • p).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) = (RingHom.id R) a • p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)

Tactic:
by
    dsimp; rw [sum_smul_index] <;>
      simp only [mul_sum, ← C_mul', mul_assoc, map_mul, forall_const, zero_mul, map_zero, sum]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
⊢ ↑q.natDegree ≤ ↑p.natDegree

Tactic:
rw [← degree_eq_natDegree h.2, ← degree_eq_natDegree hq0]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
⊢ q.degree ≤ p.degree
Module: Mathlib.Algebra.Polynomial.Eval.SMul

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
p : R[X]
x : R
⊢ eval x (s • p) = s • eval x p

Tactic:
← smul_one_smul R s p,

Goal state after:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
p : R[X]
x : R
⊢ eval x ((s • 1) • p) = s • eval x p
Module: Mathlib.Algebra.Polynomial.Eval.SMul

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
p q : R[X]
⊢ (s • p).comp q = s • p.comp q

Tactic:
← smul_one_smul R s p,

Goal state after:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
p q : R[X]
⊢ ((s • 1) • p).comp q = s • p.comp 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
⊢ n + 1 + 1 ≤ i

Tactic:
exact (mem_Icc.mp hi).1

Goal state after:
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ i, 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } := fun n ↦ Nat.recOn n (hs.index (x' 0) ⋯) fun n xn ↦ hs.index (x' (n + 1) ∩ s ↑xn) ⋯
x_anti : Antitone fun i ↦ s ↑(x i)
⊢ ∃ x, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun i ↦ s (x i)

Tactic:
have x_subset : ∀ i, s (x i).1 ⊆ x' i := by
    rintro (_ | i)
    exacts [hs.set_index_subset _, (hs.set_index_subset _).trans inter_subset_left]

Goal state after:
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ i, 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } := fun n ↦ Nat.recOn n (hs.index (x' 0) ⋯) fun n xn ↦ hs.index (x' (n + 1) ∩ s ↑xn) ⋯
x_anti : Antitone fun i ↦ s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
⊢ ∃ x, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun i ↦ s (x i)
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂₀ ⋃ i, σ i ⊆ U
⊢ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Tactic:
rw [sInter_iUnion] at tinter

Goal state after:
case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
⊢ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ U ∈ ⨅ i, s i → ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

pp: case mpr
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ (∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i) → U ∈ ⨅ i, s i

Tactic:
· rw [iInf_eq_generate, mem_generate_iff]
    rintro ⟨t, tsub, tfin, tinter⟩
    rcases eq_finite_iUnion_of_finite_subset_iUnion tfin tsub with ⟨I, Ifin, σ, σfin, σsub, rfl⟩
    rw [sInter_iUnion] at tinter
    set V := fun i => U ∪ ⋂₀ σ i with hV
    have V_in : ∀ (i : I), V i ∈ s i := by
      rintro i
      have : ⋂₀ σ i ∈ s i := by
        rw [sInter_mem (σfin _)]
        apply σsub
      exact mem_of_superset this subset_union_right
    refine ⟨I, Ifin, V, V_in, ?_⟩
    rwa [hV, ← union_iInter, union_eq_self_of_subset_right]

Goal state after:
case mpr
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ (∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i) → U ∈ ⨅ i, s i
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
this : (g.comp (X + C t)).coeff 0 = eval t g
⊢ eval t g = ((X + C t - C t) ^ m * g.comp (X + C t)).trailingCoeff

Tactic:
add_sub_cancel_right,

Goal state after:
case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
this : (g.comp (X + C t)).coeff 0 = eval t g
⊢ eval t g = (X ^ m * g.comp (X + C t)).trailingCoeff
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ (X - C x) ^ (rootMultiplicity x p + rootMultiplicity x q) ∣ p * q

Tactic:
pow_add

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ (X - C x) ^ rootMultiplicity x p * (X - C x) ^ rootMultiplicity x q ∣ p * q
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
⊢ s ∈ f i

Tactic:
rcases mem_pi.1 (mem_map.1 hs) with ⟨I, hIf, t, htf, hI⟩

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : I.pi t ⊆ eval i ⁻¹' s
⊢ s ∈ f i
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ (f ×ˢ g).NeBot ↔ f.NeBot ∧ g.NeBot

Tactic:
simp only [neBot_iff, Ne, prod_eq_bot, not_or]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℤ
⊢ derivative ↑n = 0

Tactic:
rw [← C_eq_intCast n]
  exact derivative_C

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

Goal state before:
pp: case left_neg
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
r : Finset R × R
hr :
  r ∈
    {x ∈ powersetCard (#S - k) S ×ˢ S |
      match x with
      | (T, i) => i ∈ T}
⊢ (match
      match r, hr with
      | (T, i), x => (T.erase i, i),
      ⋯ with
    | (T, i), x => (insert i T, i)) =
    r

Tactic:
dsimp at hr ⊢

Goal state after:
case left_neg
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
r : Finset R × R
hr : r ∈ {x ∈ powersetCard (#S - k) S ×ˢ S | x.2 ∈ x.1}
⊢ (insert r.2 (r.1.erase r.2), r.2) = r
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
p : M₀
hp : Prime p
s✝ : Multiset M₀
a : M₀
s : Multiset M₀
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q

Tactic:
rcases hp.dvd_or_dvd hps with h | h

Goal state after:
case inl
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
p : M₀
hp : Prime p
s✝ : Multiset M₀
a : M₀
s : Multiset M₀
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
h : p ∣ a
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q

case inr
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
p : M₀
hp : Prime p
s✝ : Multiset M₀
a : M₀
s : Multiset M₀
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
h : p ∣ s.prod
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case right_neg
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
r : Finset R × R
hr :
  r ∈
    {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
      match x with
      | (T, i) => i ∉ T}
⊢ (match
      match r, hr with
      | (T, i), x => (insert i T, i),
      ⋯ with
    | (T, i), x => (T.erase i, i)) =
    r

Tactic:
dsimp at hr ⊢

Goal state after:
case right_neg
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
r : Finset R × R
hr : r ∈ {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S | x.2 ∉ x.1}
⊢ ((insert r.2 r.1).erase r.2, r.2) = r
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
d : σ →₀ ℕ
hd : d ∈ {d | (weight w) d ≤ n}
⊢ d ∈ ↑(Finset.image (fun uv ↦ uv.1) fg)

Tactic:
rw [hfg]

Goal state after:
σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
d : σ →₀ ℕ
hd : d ∈ {d | (weight w) d ≤ n}
⊢ d ∈ ↑(Finset.image (fun uv ↦ uv.1) (Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))))
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ (-1 • p).roots = p.roots

Tactic:
roots_smul_nonzero p (neg_ne_zero.mpr one_ne_zero)

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ p.roots = p.roots
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case mp
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x ∣ y → normalizedFactors x ≤ normalizedFactors y

Tactic:
rintro ⟨c, rfl⟩

Goal state after:
case mp
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
c : α
hy : x * c ≠ 0
⊢ normalizedFactors x ≤ normalizedFactors (x * c)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
this : (normalizedFactors r).prod ~ᵤ r
⊢ p ^ (normalizedFactors r).card ~ᵤ r

Tactic:
Multiset.eq_replicate_of_mem fun b => h,

Goal state after:
case h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
this : (Multiset.replicate (normalizedFactors r).card p).prod ~ᵤ r
⊢ p ^ (normalizedFactors r).card ~ᵤ r
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
n : ℕ
hη : 0 ∈ nthRootsFinset (n + 1) a
⊢ False

Tactic:
rw [mem_nthRootsFinset n.succ_pos, zero_pow n.succ_ne_zero] at hη
    exact ha hη.symm

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
k : ℕ
⊢ Associated (C r * X ^ k).content r

Tactic:
grw [associated_content_C_mul, content_X_pow, mul_one]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
k : ℕ
⊢ Associated r r
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing T
p : T[X]
inst✝⁴ : CommRing S
inst✝³ : Algebra T S
inst✝² : Algebra S R
inst✝¹ : Algebra T R
inst✝ : IsScalarTower T S R
⊢ (map ((algebraMap S R).comp (algebraMap T S)) p).roots = (map (algebraMap T R) p).roots

Tactic:
IsScalarTower.algebraMap_eq T S R

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing T
p : T[X]
inst✝⁴ : CommRing S
inst✝³ : Algebra T S
inst✝² : Algebra S R
inst✝¹ : Algebra T R
inst✝ : IsScalarTower T S R
⊢ (map ((algebraMap S R).comp (algebraMap T S)) p).roots = (map ((algebraMap S R).comp (algebraMap T S)) p).roots
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case pos
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
h : p ∣ b
⊢ ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b

pp: case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
h : ¬p ∣ b
⊢ ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b

Tactic:
· rcases h with ⟨b, rfl⟩
      obtain ⟨a', b', c', no_factor, ha', hb'⟩ := ih_a a_ne_zero b
      refine ⟨a', b', p * c', @no_factor, ?_, ?_⟩
      · rw [mul_assoc, ha']
      · rw [mul_assoc, hb']

Goal state after:
case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
h : ¬p ∣ b
⊢ ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : WithTop (Multiset { a // Irreducible a })
h : prod p = prod q
⊢ p = q

Tactic:
induction p <;> induction q

Goal state after:
case top.top
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
h : prod ⊤ = prod ⊤
⊢ ⊤ = ⊤

case top.coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ⊤ = prod ↑a✝
⊢ ⊤ = ↑a✝

case coe.top
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝ = prod ⊤
⊢ ↑a✝ = ⊤

case coe.coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
⊢ ↑a✝¹ = ↑a✝
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ p ∣ a → Associates.mk p ∈ (Associates.mk a).factors

Tactic:
apply mem_factors_of_dvd ha0 hp

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

Goal state before:
pp: R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hf : eval₂ ϕ α f = 0
hg : eval₂ ϕ α g = 0
⊢ eval₂ ϕ α (f * EuclideanDomain.gcdA f g) + eval₂ ϕ α (g * EuclideanDomain.gcdB f g) = 0

Tactic:
Polynomial.eval₂_mul,

Goal state after:
R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hf : eval₂ ϕ α f = 0
hg : eval₂ ϕ α g = 0
⊢ eval₂ ϕ α f * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α (g * EuclideanDomain.gcdB f g) = 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hf : eval₂ ϕ α f = 0
hg : eval₂ ϕ α g = 0
⊢ eval₂ ϕ α f * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α (g * EuclideanDomain.gcdB f g) = 0

Tactic:
Polynomial.eval₂_mul,

Goal state after:
R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hf : eval₂ ϕ α f = 0
hg : eval₂ ϕ α g = 0
⊢ eval₂ ϕ α f * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α g * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0