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

Goal state before:
pp: case ind.zero
b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
⊢ ((b + 2).digits n.succ)[0]?.getD 0 = n.succ / (b + 2) ^ 0 % (b + 2)

Tactic:
← List.head?_eq_getElem?,

Goal state after:
case ind.zero
b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
⊢ ((b + 2).digits n.succ).head?.getD 0 = n.succ / (b + 2) ^ 0 % (b + 2)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: n b : ℕ
hb : 1 < b
l i : ℕ
hi : i ∈ b.digitsAppend l n
⊢ i < b

Tactic:
rw [digitsAppend, mem_append, mem_replicate] at hi
  obtain hi | ⟨_, rfl⟩ := hi
  · exact digits_lt_base hb hi
  · linarith

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

Goal state before:
pp: n p : ℕ
hp : ¬Prime p
⊢ n.factorization p = 0

Tactic:
simp [factorization_eq_zero_iff, hp]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
Nat.mod_eq_zero_of_dvd h,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : orderOf x ∣ n
⊢ x ^ 0 = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : orderOf x ∣ n
⊢ x ^ n = 1

Tactic:
rw [← pow_mod_orderOf, Nat.mod_eq_zero_of_dvd h, _root_.pow_zero]

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

Goal state before:
pp: n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), m.factorization p = 0
⊢ ∑ i ∈ Ico 1 (p * n + 1), i.factorization p +
      (∑ k ∈ Ico (p * n + 1) (p * (n + 1)), k.factorization p + (1 + (n + 1).factorization p)) =
    ∑ x ∈ Ico 1 (p * n + 1), x.factorization p + ((n + 1).factorization p + 1)

Tactic:
sum_congr rfl h4,

Goal state after:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), m.factorization p = 0
⊢ ∑ i ∈ Ico 1 (p * n + 1), i.factorization p +
      (∑ x ∈ Ico (p * n + 1) (p * (n + 1)), 0 + (1 + (n + 1).factorization p)) =
    ∑ x ∈ Ico 1 (p * n + 1), x.factorization p + ((n + 1).factorization p + 1)
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
hkn : k ≤ n
⊢ (n.choose k).factorization p ≤ log p n

Tactic:
factorization_choose hp hkn (Nat.lt_add_one _)

Goal state after:
case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
hkn : k ≤ n
⊢ #({i ∈ Ico 1 (log p n + 1) | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}) ≤ log p n
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
h : ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x ≠ ⊤
⊢ ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + (1 + emultiplicity p (n + 1)) = emultiplicity p (n + 1) + 1

Tactic:
sum_congr rfl h4,

Goal state after:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
h : ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x ≠ ⊤
⊢ ∑ x ∈ Ico (p * n + 1) (p * (n + 1)), 0 + (1 + emultiplicity p (n + 1)) = emultiplicity p (n + 1) + 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
hG : ∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a
n : ℕ
hn : n ≠ 0
a b : G
hab : (fun a ↦ a ^ n) a / (fun a ↦ a ^ n) b = 1
⊢ a / b = 1

Tactic:
simp only [← div_pow, isOfFinOrder_iff_pow_eq_one] at hab hG

Goal state after:
G : Type u_1
inst✝ : CommGroup G
n : ℕ
hn : n ≠ 0
a b : G
hab : (a / b) ^ n = 1
hG : ∀ ⦃a : G⦄, a ≠ 1 → ¬∃ n, 0 < n ∧ a ^ n = 1
⊢ a / b = 1
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case refine_2.inr.inl
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 : M p
hq : q.natDegree = 0
⊢ (p + q).natDegree = 0 ∨ M (p + q)

Tactic:
refine Or.inr ?_
      rw [eq_C_of_natDegree_eq_zero hq, add_comm]
      exact h_C_add hp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∑ x ∈ antidiagonal n, f.coeff (x.1 * p) * ((expand R p) g).coeff (x.2 * p) =
    ∑ x ∈ antidiagonal n, (contract p f).coeff x.1 * g.coeff x.2

Tactic:
coeff_expand_mul hp.bot_lt,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∑ x ∈ antidiagonal n, f.coeff (x.1 * p) * g.coeff x.2 = ∑ x ∈ antidiagonal n, (contract p f).coeff x.1 * g.coeff x.2
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg.succ.inl
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : f.coeff (n + 1) = 0
⊢ 0 = f.coeff (n + 1)

Tactic:
h'

Goal state after:
case neg.succ.inl
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : f.coeff (n + 1) = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
ha : a = x
⊢ count x (x ::ₘ t) = 1 + count x t

Tactic:
count_cons_self,

Goal state after:
case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
ha : a = x
⊢ count x t + 1 = 1 + count x t
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
n : ℕ
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
⊢ ¬(n + 1 = 0 ∨ p.coeff (n + 1) = 0) ↔ p.coeff (n + 1) ≠ 0

Tactic:
simp only [Nat.succ_ne_zero, false_or]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : derivative (p ^ (n + 1)) = C (↑n + 1) * p ^ n * derivative p
⊢ C (↑n + 1) * p ^ n * p * derivative p + p ^ n.succ * derivative p = C (↑n.succ + 1) * p ^ n.succ * derivative p

Tactic:
C_add,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : derivative (p ^ (n + 1)) = C (↑n + 1) * p ^ n * derivative p
⊢ (C ↑n + C 1) * p ^ n * p * derivative p + p ^ n.succ * derivative p = C (↑n.succ + 1) * p ^ n.succ * derivative p
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
⊢ ∀ (i' : Set ι × ((i : ι) → Set (α i))),
    (i'.1.Finite ∧ ∀ i ∈ i'.1, i'.2 i ∈ l i) → (Pi.map f '' i'.1.pi fun i ↦ id (i'.2 i)) ∈ pi fun i ↦ map (f i) (l i)

Tactic:
rintro ⟨I, s⟩ ⟨hI : I.Finite, hs : ∀ i ∈ I, s i ∈ l i⟩

Goal state after:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
⊢ (Pi.map f '' (I, s).1.pi fun i ↦ id ((I, s).2 i)) ∈ pi fun i ↦ map (f i) (l i)
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case pos
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : {y | f y < x}.Finite
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
obtain ⟨a₀, ⟨ha₀ : f a₀ < x, ha₀s⟩, others_bigger⟩ :=
      exists_min_image _ f (this.inter_of_left s) ⟨y, hx, hys⟩

Goal state after:
case pos
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : {y | f y < x}.Finite
a₀ : α
others_bigger : ∀ b ∈ {y | f y < x} ∩ s, f a₀ ≤ f b
ha₀ : f a₀ < x
ha₀s : a₀ ∈ s
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ (map (fun x ↦ b) (𝓟 {a})).coprod (map id (𝓟 {i})) = 𝓟 ({b} ×ˢ univ ∪ univ ×ˢ {i})

Tactic:
simp only [map_principal, Filter.coprod, comap_principal, sup_principal, image_singleton,
    prod_univ, univ_prod, id]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
P : R[X]
h : P.degree < ↑0
⊢ (⇑derivative)^[0] P = 0

Tactic:
case =>

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
k : ℕ
ind : ∀ {P : R[X]}, P.degree < ↑k → (⇑derivative)^[k] P = 0
P : R[X]
h : P.degree < ↑(k + 1)
hP : P = 0
⊢ (⇑derivative)^[k + 1] P = 0

Tactic:
case =>

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
k : ℕ
ind : ∀ {P : R[X]}, P.degree < ↑k → (⇑derivative)^[k] P = 0
P : R[X]
h : P.degree < ↑(k + 1)
hP : ¬P = 0
hP' : derivative P = 0
⊢ (⇑derivative)^[k] (derivative P) = 0

Tactic:
case =>

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
k : ℕ
ind : ∀ {P : R[X]}, P.degree < ↑k → (⇑derivative)^[k] P = 0
P : R[X]
h : P.degree < ↑(k + 1)
hP : ¬P = 0
hP' : ¬derivative P = 0
⊢ (⇑derivative)^[k] (derivative P) = 0

Tactic:
case =>

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
k : ℕ
ind : ∀ {P : R[X]}, P.degree < ↑k → (⇑derivative)^[k] P = 0
P : R[X]
h : P.degree < ↑(k + 1)
hP : ¬P = 0
⊢ (⇑derivative)^[k + 1] P = 0

Tactic:
case =>

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
k : ℕ
ind : ∀ {P : R[X]}, P.degree < ↑k → (⇑derivative)^[k] P = 0
P : R[X]
h : P.degree < ↑(k + 1)
⊢ (⇑derivative)^[k + 1] P = 0

Tactic:
case =>

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
hk : 0 ≤ #S
⊢ (⇑derivative)^[0] (∏ a ∈ S, (X - C a)) = ↑0! * ∑ T ∈ powersetCard (#S - 0) S, ∏ a ∈ T, (X - C a)

Tactic:
case =>

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : k ≤ #S → (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ (⇑derivative)^[k + 1] (∏ a ∈ S, (X - C a)) = ↑(k + 1)! * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a)

Tactic:
case =>

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
P : R[X]
h : P ∣ derivative P
hP : P = 0
⊢ derivative P = 0

pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
P : R[X]
h : P ∣ derivative P
hP : ¬P = 0
⊢ derivative P = 0

Tactic:
· simp only [hP, derivative_zero]

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
P : R[X]
h : P ∣ derivative P
hP : ¬P = 0
⊢ derivative P = 0
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_5
inst✝² : AddCommMonoid R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : s ∈ f.support
⊢ f s ≤ degree f

Tactic:
exact Finset.single_le_sum_of_canonicallyOrdered h

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

Goal state before:
pp: σ : Type u_1
M : Type u_2
τ : Type u_5
f : σ → τ
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : CanonicallyOrderedAdd M
x : τ →₀ M
hf : Set.InjOn f (f ⁻¹' ↑x.support)
⊢ degree (comapDomain f x hf) ≤ degree x

Tactic:
simpa [degree, comapDomain, Finset.sum_preimage' f x.support hf x] using
    Finset.sum_le_sum_of_subset (Finset.filter_subset ..)

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * ↑u = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ ¬IsUnit (p * ↑u * (s.erase q).prod)

Tactic:
apply mt isUnit_of_mul_isUnit_left (mt isUnit_of_mul_isUnit_left _)

Goal state after:
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * ↑u = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ ¬IsUnit p
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case succ
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
⊢ normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x

Tactic:
by_cases h0 : x = 0

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
h0 : x = 0
⊢ normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x

case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
h0 : ¬x = 0
⊢ normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case empty
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
hs : ∀ a ∈ 0, Irreducible a
⊢ normalizedFactors (Multiset.prod 0) = Multiset.map normalize 0

Tactic:
Multiset.prod_zero,

Goal state after:
case empty
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
hs : ∀ a ∈ 0, Irreducible a
⊢ normalizedFactors 1 = Multiset.map normalize 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
⊢ Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)

Tactic:
by_cases h0 : x = 0

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : x = 0
⊢ Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)

case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
η₁ η₂ a₁ a₂ : R
n : ℕ
hη₁ : η₁ ∈ nthRootsFinset (n + 1) a₁
hη₂ : η₂ ∈ nthRootsFinset (n + 1) a₂
⊢ η₁ * η₂ ∈ nthRootsFinset (n + 1) (a₁ * a₂)

Tactic:
rw [mem_nthRootsFinset n.succ_pos] at hη₁ hη₂ ⊢

Goal state after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
η₁ η₂ a₁ a₂ : R
n : ℕ
hη₁ : η₁ ^ n.succ = a₁
hη₂ : η₂ ^ n.succ = a₂
⊢ (η₁ * η₂) ^ n.succ = a₁ * a₂
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case pos.refine_1
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 a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * c' * a' = p * a

pp: case pos.refine_2
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 a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * c' * b' = p * b

Tactic:
· rw [mul_assoc, ha']

Goal state after:
case pos.refine_2
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 a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * c' * b' = p * b
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ eval t ((⇑derivative)^[m - 0] ((X - C t) ^ m)) * eval t ((⇑derivative)^[0] (p /ₘ (X - C t) ^ m)) =
    m ! • eval t (p /ₘ (X - C t) ^ m)

Tactic:
m.sub_zero,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ eval t ((⇑derivative)^[m] ((X - C t) ^ m)) * eval t ((⇑derivative)^[0] (p /ₘ (X - C t) ^ m)) =
    m ! • eval t (p /ₘ (X - C t) ^ m)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case top
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : Nontrivial α
⊢ prod ⊤ = 0 ↔ ⊤ = ⊤

pp: case coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ prod ↑a✝ = 0 ↔ ↑a✝ = ⊤

Tactic:
· simp only [Associates.prod_top]

Goal state after:
case coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ prod ↑a✝ = 0 ↔ ↑a✝ = ⊤
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 0
⊢ p.degree ≤ 0

Tactic:
by simp [*]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
⊢ ↑(∏ i ∈ s, map (algebraMap R S) (f i)).roots.toFinset = ⋃ i ∈ ↑s, ↑(map (algebraMap R S) (f i)).roots.toFinset

Tactic:
roots_prod,

Goal state after:
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
⊢ ↑(s.val.bind fun i ↦ (map (algebraMap R S) (f i)).roots).toFinset =
    ⋃ i ∈ ↑s, ↑(map (algebraMap R S) (f i)).roots.toFinset

case a
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
⊢ ∏ i ∈ s, map (algebraMap R S) (f i) ≠ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
⊢ p = FactorSet.prod ↑{⟨p, hp⟩}

Tactic:
FactorSet.prod.eq_def

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
⊢ p =
    match ↑{⟨p, hp⟩} with
    | none => 0
    | some s => (Multiset.map Subtype.val s).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
k : ℕ
⊢ p ^ k = FactorSet.prod ↑(replicate k ⟨p, hp⟩)

Tactic:
FactorSet.prod.eq_def

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
k : ℕ
⊢ p ^ k =
    match ↑(replicate k ⟨p, hp⟩) with
    | none => 0
    | some s => (Multiset.map Subtype.val s).prod
Module: Mathlib.Algebra.AlgebraicCard

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
⊢ lift.{v, u} #R[X] * ℵ₀ ≤ max (lift.{v, u} #R) ℵ₀

Tactic:
by grw [lift_le.2 cardinalMk_le_max]; simp

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

Goal state before:
pp: K : Type u
inst✝² : CommSemiring K
D : Type v
inst✝¹ : Semiring D
inst✝ : Algebra K D
h : IsCentral K D
x : D
⊢ x ∈ Set.range ⇑(algebraMap K D) ↔ ∃ a, x = (algebraMap K D) a

Tactic:
simp [eq_comm]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
A : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : NoZeroDivisors S
inst✝⁴ : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
inj : Injective ⇑(algebraMap R A)
s : S
eq : (algebraMap S A) s = 0
ne✝ : ¬s = 0
r : R
ne : r ≠ 0
dvd : s ∣ (algebraMap R S) r
⊢ (algebraMap S A) s ∣ (algebraMap R A) r

Tactic:
IsScalarTower.algebraMap_apply R S A,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
A : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : NoZeroDivisors S
inst✝⁴ : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
inj : Injective ⇑(algebraMap R A)
s : S
eq : (algebraMap S A) s = 0
ne✝ : ¬s = 0
r : R
ne : r ≠ 0
dvd : s ∣ (algebraMap R S) r
⊢ (algebraMap S A) s ∣ (algebraMap S A) ((algebraMap R S) r)
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
i : ι
x : M ⊗[R] G i
⊢ (LinearMap.lTensor M (f i i ⋯)) x = x

Tactic:
convert! LinearMap.lTensor_id_apply M _ x

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
i : ι
x : M ⊗[R] G i
⊢ f i i ⋯ = LinearMap.id