mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p n : ℕ
hp : 1 < p
hn : n ≠ 0
⊢ ¬p ∣ n.divMaxPow p

Tactic:
by
  simp [divMaxPow, maxPowDvdDiv, maxPowDvdDiv.go_spec, *]

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

Goal state before:
pp: case h₁
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ k ≤ (p.maxPowDvdDiv n).fst

Tactic:
← padicValNat,

Goal state after:
case h₁
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ k ≤ padicValNat p n
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case h
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ p ^ (padicValNat p n + k) * n.divMaxPow p = p ^ k * n

pp: case hl
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ ¬p ∣ n.divMaxPow p

Tactic:
· rw [Nat.pow_add, Nat.mul_assoc, Nat.mul_left_comm, pow_padicValNat_mul_divMaxPow]

Goal state after:
case hl
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ ¬p ∣ n.divMaxPow p
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b m n : ℕ
⊢ ofDigits b (b.digits n) + b ^ (b.digits n).length * ofDigits b (b.digits m) = n + b ^ (b.digits n).length * m

Tactic:
ofDigits_digits,

Goal state after:
b m n : ℕ
⊢ n + b ^ (b.digits n).length * ofDigits b (b.digits m) = n + b ^ (b.digits n).length * m
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: case inr
p n : ℕ
hp : p ≠ 1
⊢ (emultiplicity p n).toNat = padicValNat p n

Tactic:
· rcases eq_or_ne n 0 with rfl | hn
    · simp
    · simp [← padicValNat_eq_emultiplicity_of_ne_one, *]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case empty
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
β : Type u_3
p : α
hp : Prime p
f : β → α
⊢ emultiplicity p 1 = 0

Tactic:
exact emultiplicity_of_one_right hp.not_isUnit

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

Goal state before:
pp: a b : ℕ
hb : b ≠ 0
⊢ a.factorization ≤ (a * b).factorization

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Goal state after:
case inl
b : ℕ
hb : b ≠ 0
⊢ factorization 0 ≤ (0 * b).factorization

case inr
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ a.factorization ≤ (a * b).factorization
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ emultiplicity p n ! + emultiplicity p (n + 1) = ↑(∑ i ∈ Ico 1 b, n / p ^ i) + ↑(#({i ∈ Ico 1 b | p ^ i ∣ n + 1}))

Tactic:
rw [emultiplicity_factorial hp ((log_mono_right <| le_succ _).trans_lt hb), ←
          emultiplicity_eq_card_pow_dvd hp.ne_one (succ_pos _) hb]

Goal state after:
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
p : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x - y) ^ p = x ^ p - y ^ p

Tactic:
simp [eq_sub_iff_add_eq, ← add_pow_expChar_of_commute _ (h.sub_left rfl)]

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

Goal state before:
pp: n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n < p ^ b
⊢ {i ∈ Ico 1 n | p ^ i ∣ n} = {i ∈ Ico 1 b | p ^ i ∣ n}

Tactic:
ext i
  simp only [Finset.mem_filter, mem_Ico, and_congr_left_iff, and_congr_right_iff]
  refine fun h1 h2 ↦ ⟨fun h ↦ ?_, fun h ↦ lt_of_pow_dvd_right hn (Prime.one_lt pp) h1⟩
  rcases p with - | p
  · rw [zero_pow (by lia), zero_dvd_iff] at h1
    exact (hn h1).elim
  · rw [← Nat.pow_lt_pow_iff_right (Prime.one_lt pp)]
    apply lt_of_le_of_lt (le_of_dvd (Nat.zero_lt_of_ne_zero hn) h1) hb

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

Goal state before:
pp: case inr
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
x✝ : ∃ m, n ∣ k ^ m
m : ℕ
h : n ∣ k ^ m
hm : m ≠ 0
⊢ n.primeFactors ⊆ k.primeFactors

Tactic:
rw [← Nat.primeFactors_pow k hm]

Goal state after:
case inr
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
x✝ : ∃ m, n ∣ k ^ m
m : ℕ
h : n ∣ k ^ m
hm : m ≠ 0
⊢ n.primeFactors ⊆ (k ^ m).primeFactors
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ q = p

Tactic:
eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le hp hdvd hdeg

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ p * C q.leadingCoeff = p
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
⊢ (contract p f).coeff n = f.coeff (n * p)

Tactic:
simp only [contract, coeff_monomial, sum_ite_eq', finsetSum_coeff, mem_range, not_lt,
    ite_eq_left_iff]
  intro hn
  apply (coeff_eq_zero_of_natDegree_lt _).symm
  calc
    f.natDegree < f.natDegree + 1 := Nat.lt_succ_self _
    _ ≤ n * 1 := by simpa only [mul_one] using hn
    _ ≤ n * p := by gcongr; exact hp.bot_lt

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
h : IsUnit p
⊢ False

Tactic:
obtain ⟨u, -, h⟩ := isUnit_iff.mp h

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
h✝ : IsUnit p
u : R
h : C u = p
⊢ False
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
⊢ p %ₘ q = p

Tactic:
have : ¬degree q ≤ degree p := not_le_of_gt h
    unfold modByMonic divModByMonicAux; dsimp; rw [dif_pos hq, if_neg (mt And.left this)]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
⊢ map (frobenius R p) ((expand R p) f) = f ^ p

Tactic:
refine f.induction_on' (fun a b ha hb => ?_) fun n a => ?_

Goal state after:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f a b : R[X]
ha : map (frobenius R p) ((expand R p) a) = a ^ p
hb : map (frobenius R p) ((expand R p) b) = b ^ p
⊢ map (frobenius R p) ((expand R p) (a + b)) = (a + b) ^ p

case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ map (frobenius R p) ((expand R p) ((monomial n) a)) = (monomial n) a ^ p
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
⊢ ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ) =
    (m.succ + k).descFactorial k.succ • p.coeff (m + k.succ)

Tactic:
← Nat.succ_add,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
⊢ ((m + 1) * (m.succ + k).descFactorial k) • p.coeff (m + k.succ) =
    (m.succ + k).descFactorial k.succ • p.coeff (m + k.succ)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
a✝ : Nontrivial R
this : (X - C a).Monic
⊢ (p /ₘ (X - C a)).coeff n = p.coeff (n + 1) + a * (p /ₘ (X - C a)).coeff (n + 1)

Tactic:
set q := p /ₘ (X - C a)

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
a✝ : Nontrivial R
this : (X - C a).Monic
q : R[X] := p /ₘ (X - C a)
⊢ q.coeff n = p.coeff (n + 1) + a * q.coeff (n + 1)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ
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)^[n + 1] (p * q) =
    ∑ k ∈ range (n + 1).succ, (n + 1).choose k • ((⇑derivative)^[n + 1 - k] p * (⇑derivative)^[k] q)

Tactic:
| succ n IH =>

Goal state after:
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
⊢ ∀ (t : Set α), t ∈ ⨅ i, l i ↔ ∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t

Tactic:
by
    intro t
    constructor
    · simp only [mem_iInf', (hl _).mem_iff]
      rintro ⟨I, hI, V, hV, -, rfl, -⟩
      choose u hu using hV
      exact ⟨⟨I, u⟩, ⟨hI, fun i _ => (hu i).1⟩, iInter₂_mono fun i _ => (hu i).2⟩
    · rintro ⟨⟨I, f⟩, ⟨hI₁, hI₂⟩, hsub⟩
      grw [← hsub]
      exact (biInter_mem hI₁).mpr fun i hi => mem_iInf_of_mem i <| (hl i).mem_of_mem <| hI₂ _ hi

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

Goal state before:
pp: α : Type u_1
a : α
⊢ (𝓟 {a}).IsCountablyGenerated

Tactic:
exact isCountablyGenerated_principal _

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

Goal state before:
pp: α : Type u_2
l : Filter α
inst✝ : l.IsCountablyGenerated
h : cofinite ≤ l
⊢ l.kerᶜ.Countable

Tactic:
by
  rcases exists_antitone_basis l with ⟨s, hs⟩
  simp only [hs.ker, iInter_true, compl_iInter]
  exact countable_iUnion fun n ↦ Set.Finite.countable <| h <| hs.mem _

Goal state after:
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: case succ
M : Type u_1
inst✝ : AddMonoid M
s : Set M
n : ℕ
IH : ⇑ofAdd '' (n • s) = (⇑ofAdd '' s) ^ n
⊢ ⇑ofAdd '' ((n + 1) • s) = (⇑ofAdd '' s) ^ (n + 1)

Tactic:
| succ n IH =>

Goal state after:
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: case succ
M : Type u_1
inst✝ : AddMonoid M
s : Set (Multiplicative M)
n : ℕ
IH : ⇑toAdd '' s ^ n = n • ⇑toAdd '' s
⊢ ⇑toAdd '' s ^ (n + 1) = (n + 1) • ⇑toAdd '' s

Tactic:
| succ n IH =>

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

Goal state before:
pp: α : Type u_2
f : Filter α
⊢ f ≤ cofinite ↔ Coheyting.boundary f = f

Tactic:
← Coheyting.inf_hnot_self,

Goal state after:
α : Type u_2
f : Filter α
⊢ f ≤ cofinite ↔ f ⊓ ￢f = f
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case e_a
R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
⊢ (Multiset.map (⇑(AddMonoidHom.mulLeft (f i)))
        (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s)).sum =
    (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum

Tactic:
AddMonoidHom.coe_mulLeft

Goal state after:
case e_a
R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
⊢ (Multiset.map (HMul.hMul (f i)) (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s)).sum =
    (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case refine_4
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = (𝓟 q.1 ⊔ q.2).ker
⊢ q = (f.ker, Coheyting.boundary f)

Tactic:
ker_sup,

Goal state after:
case refine_4
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = (𝓟 q.1).ker ∪ q.2.ker
⊢ q = (f.ker, Coheyting.boundary f)
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case refine_4.refine_3
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ Coheyting.boundary f ≤ q.2

Tactic:
hq.2.2,

Goal state after:
case refine_4.refine_3
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ Coheyting.boundary (𝓟 q.1 ⊔ q.2) ≤ q.2
Module: Mathlib.Order.Filter.TendstoCofinite

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
f : α → β
inst✝¹ : AddCommMonoid M
inst✝ : TendstoCofinite f
v : α → M
i : β
h' : i ∉ range f
⊢ mapDomain f v i = 0

Tactic:
← Set.preimage_singleton_eq_empty

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
f : α → β
inst✝¹ : AddCommMonoid M
inst✝ : TendstoCofinite f
v : α → M
i : β
h' : f ⁻¹' {i} = ∅
⊢ mapDomain f v i = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: 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
⊢ ∑ T ∈ powersetCard (#S - (k + 1)) S, ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a) =
    ∑ i ∈ powersetCard (#S - (k + 1)) S, (↑k + 1) * ∏ a ∈ i, (X - C a)

Tactic:
congr! 1 with T hT

Goal state after:
case a
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
T : Finset R
hT : T ∈ powersetCard (#S - (k + 1)) S
⊢ ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a) = (↑k + 1) * ∏ a ∈ T, (X - C a)
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
this✝ : DecidableEq (Associates M)
this : p.prod ≤ (p + (q - p)).prod
⊢ p.prod ≤ q.prod

Tactic:
add_tsub_cancel_of_le h

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
this✝ : DecidableEq (Associates M)
this : p.prod ≤ q.prod
⊢ p.prod ≤ q.prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
⊢ ∀ {f g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g

Tactic:
by
  intro f
  induction f using Multiset.induction_on with
  | empty =>
    intro g _ hg h
    exact Multiset.rel_zero_left.2 <|
      Multiset.eq_zero_of_forall_notMem fun x hx =>
        have : IsUnit g.prod := by simpa [associated_one_iff_isUnit] using h.symm
        (hg x hx).not_isUnit <|
          isUnit_iff_dvd_one.2 <| (Multiset.dvd_prod hx).trans (isUnit_iff_dvd_one.1 this)
  | cons p f ih =>
    intro g hf hg hfg
    let ⟨b, hbg, hb⟩ :=
      (exists_associated_mem_of_dvd_prod (hf p (by simp)) fun q hq => hg _ hq) <|
        hfg.dvd_iff_dvd_right.1 (show p ∣ (p ::ₘ f).prod by simp)
    have := Classical.decEq α
    rw [← Multiset.cons_erase hbg]
    exact
      Multiset.Rel.cons hb
        (ih (fun q hq => hf _ (by simp [hq]))
          (fun {q} (hq : q ∈ g.erase b) => hg q (Multiset.mem_of_mem_erase hq))
          (Associated.of_mul_left
            (by rwa [← Multiset.prod_cons, ← Multiset.prod_cons, Multiset.cons_erase hbg]) hb
            (hf p (by simp)).ne_zero))

Goal state after:
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case succ
σ : Type u_5
f : σ →₀ ℕ
n : ℕ
IH : n ≤ degree f → ∃ g ≤ f, degree g = n
hn : n + 1 ≤ degree f
⊢ ∃ g ≤ f, degree g = n + 1

Tactic:
| succ n IH =>

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
f : Multiset α
hf : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ p
⊢ Prime p

Tactic:
obtain ⟨q, hq, rfl⟩ := prime_factors_irreducible h hf

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
q : α
hq : p ~ᵤ q
hf : (∀ b ∈ {q}, Prime b) ∧ {q}.prod ~ᵤ p
⊢ Prime p
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
a✝³ : α
a✝² : a✝³ ≠ 0
x✝ : Multiset α
a✝¹ : α
a✝ : a✝¹ ∈ x✝
⊢ Prime a✝¹ ↔ Irreducible a✝¹

Tactic:
simp_rw [irreducible_iff_prime_of_existsUnique_irreducible_factors eif uif]

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
⊢ p.degree < (q * C q.leadingCoeff⁻¹).degree

Tactic:
degree_mul_leadingCoeff_inv q hq0

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
⊢ p.degree < q.degree
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case pos
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
h✝ : n = 0
⊢ 1 / (↑u).coeff 0 = (↑u⁻¹).coeff 0

Tactic:
rw [div_eq_iff_mul_eq (coeff_coe_units_zero_ne_zero u), coeff_zero_eq_eval_zero,
        coeff_zero_eq_eval_zero, ← eval_mul, ← Units.val_mul, inv_mul_cancel]

Goal state after:
case pos
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
h✝ : n = 0
⊢ eval 0 ↑1 = 1
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf' : eval a (derivative f) ≠ 0
⊢ ¬X - C a ∣ f /ₘ (X - C a)

Tactic:
contrapose hf' with h

Goal state after:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
h : X - C a ∣ f /ₘ (X - C a)
⊢ eval a (derivative f) = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
⊢ p.count (a * b).factors = p.count a.factors + p.count b.factors

Tactic:
obtain ⟨a0, nza, rfl⟩ := exists_non_zero_rep ha

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
⊢ p.count (Associates.mk a0 * b).factors = p.count (Associates.mk a0).factors + p.count b.factors
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
p : Associates α
hp : Irreducible p
⊢ ¬p.count a.factors = 0 → p.count b.factors = 0

Tactic:
← Ne

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
p : Associates α
hp : Irreducible p
⊢ p.count a.factors ≠ 0 → p.count b.factors = 0
Module: Mathlib.Algebra.AlgebraicCard

Goal state before:
pp: R A : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
⊢ #{ x // IsAlgebraic R x } ≤ #R[X] * ℵ₀

Tactic:
rw [← lift_id #_, ← lift_id #R[X]]

Goal state after:
R A : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
⊢ lift.{u, u} #{ x // IsAlgebraic R x } ≤ lift.{u, u} #R[X] * ℵ₀
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : DivisionRing A
inst✝¹ : Field R
inst✝ : Algebra R A
n : ℚ
⊢ IsAlgebraic R ↑n

Tactic:
← map_ratCast (algebraMap R A)

Goal state after:
R : Type u
A : Type v
inst✝² : DivisionRing A
inst✝¹ : Field R
inst✝ : Algebra R A
n : ℚ
⊢ IsAlgebraic R ((algebraMap R A) ↑n)
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
S : Type u_1
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Nontrivial R
⊢ ∀ (x : ↥⊥), IsAlgebraic R x

Tactic:
rintro ⟨_, x, rfl⟩

Goal state after:
R : Type u
S : Type u_1
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Nontrivial R
x : R
⊢ IsAlgebraic R ⟨(Algebra.ofId R S).toRingHom x, ⋯⟩
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
s t : Set (σ →₀ ℕ)
⊢ restrictSupport R s * restrictSupport R t ≤ restrictSupport R (s + t)

Tactic:
rw [restrictSupport_eq_span, restrictSupport_eq_span, Submodule.span_mul_span,
      Submodule.span_le, Set.mul_subset_iff]
    simp +contextual [Set.add_mem_add]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : Submodule R M
smallP : Small.{u, u_2} ↥P
smallQ : Small.{u, u_2} ↥Q
⊢ Small.{u, u_2} ↥(P ⊔ Q)

Tactic:
by
  rw [Submodule.sup_eq_range]
  exact small_range _

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case empty
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (M ⊗[R] N)
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ ∅ ⊆ ↑(mapIncl M' N').range

Tactic:
exact ⟨_, _, fg_bot, fg_bot, Set.empty_subset _⟩

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
a : A
b : ↥(Submodule.restrictScalars R I)
this : a ⊗ₜ[R] ↑b = a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] ↑b
⊢ a ⊗ₜ[R] ↑b ∈ ↑(Submodule.restrictScalars R (map includeRight I))

Tactic:
rw [this]
          simp only [Submodule.coe_restrictScalars, SetLike.mem_coe]
          apply Ideal.mul_mem_left
          -- Note: adding `includeRight` as a hint fixes a timeout https://github.com/leanprover-community/mathlib4/pull/8386
          apply Ideal.mem_map_of_mem includeRight
          exact Submodule.coe_mem b

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
s : Set ℕ := {k | x ^ k = 0}
this : s = univ
⊢ nilpotencyClass x = 0

Tactic:
change sInf _ = 0

Goal state after:
R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
s : Set ℕ := {k | x ^ k = 0}
this : s = univ
⊢ sInf {k | x ^ k = 0} = 0