mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a n : ℕ
n0 : n ≠ 0
⊢ addOrderOf ↑a = n / n.gcd a

Tactic:
rcases a with - | a
  · simp only [Nat.cast_zero, addOrderOf_zero, Nat.gcd_zero_right,
      Nat.pos_of_ne_zero n0, Nat.div_self]
  rw [← Nat.smul_one_eq_cast, addOrderOf_nsmul' _ a.succ_ne_zero, ZMod.addOrderOf_one]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
inst✝ : NeZero 0
a : ZMod 0
⊢ a.cast = ↑a.val

Tactic:
cases NeZero.ne 0 rfl

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

Goal state before:
pp: case zero
inst✝ : NeZero 0
a : ZMod 0
⊢ ↑a.val = a

Tactic:
cases NeZero.ne 0 rfl

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : NeZero 0
⊢ Nat.cast ∘ val = cast

Tactic:
cases NeZero.ne 0 rfl

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

Goal state before:
pp: case zero
inst✝ : NeZero 0
⊢ Injective val

Tactic:
cases NeZero.ne 0 rfl

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

Goal state before:
pp: case zero
inst✝ : NeZero 0
a b : ZMod 0
⊢ (a + b).val = (a.val + b.val) % 0

Tactic:
cases NeZero.ne 0 rfl

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n m : ℕ
⊢ n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0

Tactic:
rcases eq_or_ne m 0 with (rfl | hm); · simp [divisors]
  simp only [hm, Ne, not_false_iff, and_true, ← filter_dvd_eq_divisors hm, mem_filter,
    mem_range, and_iff_right_iff_imp, Nat.lt_succ_iff]
  exact le_of_dvd hm.bot_lt

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.divisors.Nonempty ↔ n ≠ 0

Tactic:
exact nonempty_divisors

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

Goal state before:
pp: case succ.succ.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : 0 ≤ x
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i

Tactic:
exact geom_sum_pos hx' (by simp)

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ z.divisors.Nonempty ↔ z ≠ 0

Tactic:
exact nonempty_divisors

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

Goal state before:
pp: case mp
n : ℕ
⊢ Subsingleton (ZMod n) → n = 1

pp: case mpr
n : ℕ
⊢ n = 1 → Subsingleton (ZMod n)

Tactic:
· obtain (_ | _ | n) := n
    · simpa [ZMod] using not_subsingleton _
    · simp [ZMod]
    · simpa [ZMod] using not_subsingleton _

Goal state after:
case mpr
n : ℕ
⊢ n = 1 → Subsingleton (ZMod n)
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ ↑r ! * ↑(n.choose r) ≤ ↑n ^ r

pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ 0 < ↑r !

Tactic:
· norm_cast
    rw [← Nat.descFactorial_eq_factorial_mul_choose]
    exact n.descFactorial_le_pow r

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ 0 < ↑r !
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b m : ℕ
hb : 1 < b
hm : 0 < m
⊢ b.digits (b * m) = 0 :: b.digits m

Tactic:
digits_def' hb (by positivity)

Goal state after:
b m : ℕ
hb : 1 < b
hm : 0 < m
⊢ b * m % b :: b.digits (b * m / b) = 0 :: b.digits m
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : FiniteMultiplicity a b
⊢ emultiplicity a b = ↑(multiplicity a b)

Tactic:
cases hm : emultiplicity a b
  · simp [h] at hm
  rw [multiplicity_eq_of_emultiplicity_eq_some hm]

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

Goal state before:
pp: n : ℕ
⊢ n.factorization = Multiset.toFinsupp ↑n.primeFactorsList

Tactic:
by
  ext p
  simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ f x ^ n = 1

Tactic:
rw [← f.map_pow, hn, f.map_one]

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 : n = 0
⊢ False

Tactic:
by simp [hx, hn0] at ha

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 ↔ k ≤ n.factorization p

Tactic:
by
  rw [← factorization_le_iff_dvd (Nat.pow_pos pp.pos).ne' hn, pp.factorization_pow, single_le_iff]

Goal state after:
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
⊢ #({i ∈ Ico 1 (log p n + 1) | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}) ≤ log p n

Tactic:
exact (card_filter_le ..).trans_eq (Nat.card_Ico _ _)

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

Goal state before:
pp: m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
fin : FiniteMultiplicity m n
i : ℕ
⊢ 1 ≤ i → i ≤ multiplicity m n → i < b

Tactic:
intro hi h

Goal state after:
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
fin : FiniteMultiplicity m n
i : ℕ
hi : 1 ≤ i
h : i ≤ multiplicity m n
⊢ i < b
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case succ
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
m : ℕ
hm : m + 1 ≠ 1
hb : log (m + 1) n < b
fin : FiniteMultiplicity (m + 1) n
h : (m + 1) ^ i ∣ n
⊢ i ≤ log (m + 1) n

Tactic:
exact le_log_of_pow_le (one_lt_iff_ne_zero_and_ne_one.2 ⟨m.succ_ne_zero, hm⟩)
                (le_of_dvd hn h)

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
← orderOf_eq_zero_iff

Goal state after:
case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : IsMulTorsionFree G
g : G
ha : orderOf g = 0
⊢ orderOf g ≤ 1
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
this : (n + k).choose k * k ! * n ! = (n + k)!
⊢ emultiplicity p (n + k)! = ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) + emultiplicity p (k ! * n !)

Tactic:
hp.emultiplicity_factorial hnb,

Goal state after:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
this : (n + k).choose k * k ! * n ! = (n + k)!
⊢ ↑(∑ i ∈ Ico 1 b, (n + k) / p ^ i) = ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) + emultiplicity p (k ! * n !)
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
⊢ x %ᵒᶠ g + of' k G g * (x /ᵒᶠ g) = x

Tactic:
rw [add_comm, divOf_add_modOf]

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

Goal state before:
pp: case φ_k
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (f : R[X]), f.natDegree < 1 → divX_hom f = 0

pp: case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → (divX_hom ((monomial n) c)).natDegree = n - 1

Tactic:
· intro f
    simpa [divX_hom, divX_eq_zero_iff] using eq_C_of_natDegree_eq_zero

Goal state after:
case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → (divX_hom ((monomial n) c)).natDegree = n - 1
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p.divX * X + C (p.coeff 0) = 0
wf : (p.divX * X + C (p.coeff 0)).divX.degree < (p.divX * X + C (p.coeff 0)).degree
hcp0 : p.coeff 0 = 0
h : p.divX = 0
⊢ False

Tactic:
by simp [h, hcp0] at hp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
⊢ orderOf x = orderOf y

Tactic:
rw [orderOf_eq_orderOf_iff]

Goal state after:
G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
⊢ ∀ (n : ℕ), x ^ n = 1 ↔ y ^ n = 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
⊢ ¬p /ₘ q = 0

Tactic:
divByMonic_eq_zero_iff hq,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
⊢ ¬p.degree < q.degree
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
_x : (p : R[X]) ×' p ≠ 0
a✝¹ :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun p x ↦ p.natDegree) y _x →
      ∃ s, ↑s.card ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p✝ : R[X]
x✝¹ : p✝ ≠ 0
a✝ :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun p x ↦ p.natDegree) y ⟨p✝, x✝¹⟩ →
      ∃ s, ↑s.card ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p : R[X]
hp : p ≠ 0
x✝ :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun p x ↦ p.natDegree) y ⟨p, hp⟩ →
      ∃ s, ↑s.card ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
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
⊢ (p /ₘ (X - C x)).natDegree < p.natDegree

Tactic:
apply (Nat.cast_lt (α := WithBot ℕ)).mp

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
_x : (p : R[X]) ×' p ≠ 0
a✝¹ :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun p x ↦ p.natDegree) y _x →
      ∃ s, ↑s.card ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p✝ : R[X]
x✝¹ : p✝ ≠ 0
a✝ :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun p x ↦ p.natDegree) y ⟨p✝, x✝¹⟩ →
      ∃ s, ↑s.card ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p : R[X]
hp : p ≠ 0
x✝ :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun p x ↦ p.natDegree) y ⟨p, hp⟩ →
      ∃ s, ↑s.card ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
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
⊢ ↑(p /ₘ (X - C x)).natDegree < ↑p.natDegree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : p.IsRoot a
⊢ p = (X - C a) * (p /ₘ (X - C a))

Tactic:
by rw [mul_divByMonic_eq_iff_isRoot.2 h]

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

Goal state before:
pp: case refine_1
α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : ⦃i : ι⦄ → ⦃j : ι⦄ → { s // s ∈ l i }
t : ⦃i : ι⦄ → ⦃j : ι⦄ → { t // t ∈ l j }
hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ↑s ↑t
i : ι
⊢ (fun i ↦ ⋂ j, ↑s ∩ ↑t) i ∈ l i

pp: case refine_2
α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : ⦃i : ι⦄ → ⦃j : ι⦄ → { s // s ∈ l i }
t : ⦃i : ι⦄ → ⦃j : ι⦄ → { t // t ∈ l j }
hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ↑s ↑t
i j : ι
hij : i ≠ j
⊢ (Disjoint on fun i ↦ ⋂ j, ↑s ∩ ↑t) i j

Tactic:
exacts [iInter_mem.2 fun j => inter_mem (@s i j).2 (@t j i).2,
    (hst hij).mono ((iInter_subset _ j).trans inter_subset_left)
      ((iInter_subset _ i).trans inter_subset_right)]

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

Goal state before:
pp: α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋃ x, f ↑x ≤ᶠ[l] ⋃ x, g ↑x

Tactic:
exact .iUnion fun i ↦ hle i.1 i.2

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
by_cases! all_top : ∃ y ∈ s, ∃ x, f y < x

Goal state after:
case pos
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
all_top : ∃ y ∈ s, ∃ x, f y < x
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

case neg
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
all_top : ∀ y ∈ s, ∀ (x : β), x ≤ f y
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
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₀ : α
others_bigger : ∀ b ∈ {y | f y < x} ∩ s, f a₀ ≤ f b
ha₀ : f a₀ < x
ha₀s : a₀ ∈ s
a : α
has : a ∈ s
⊢ f a < x → f a₀ ≤ f a

Tactic:
exact fun h => others_bigger a ⟨h, has⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f.coprod g = f ×ˢ ⊤ ⊔ ⊤ ×ˢ g

Tactic:
rw [prod_top, top_prod]

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f.coprod g = comap Prod.fst f ⊔ comap Prod.snd g
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
⊢ (⇑derivative)^[k + 1] (∏ a ∈ S, (X - C a)) = ↑(k + 1)! * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a)

Tactic:
nth_rewrite 1 [add_comm]

Goal state after:
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
⊢ (⇑derivative)^[1 + k] (∏ a ∈ S, (X - C a)) = ↑(k + 1)! * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a)
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
⊢ q / GCDMonoid.gcd p q ≠ 0

Tactic:
obtain ⟨r, hr⟩ := GCDMonoid.gcd_dvd_right p q

Goal state after:
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
⊢ q / GCDMonoid.gcd p q ≠ 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) =
    (↑k + 1) * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a)

Tactic:
rw [mul_sum]
        congr! 1 with T hT
        simp [sum_const, show #(S \ T) = k + 1 by grind]

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

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

Tactic:
case succ k ind =>
    specialize ind (Nat.le_of_succ_le hk)
    nth_rewrite 1 [add_comm]
    rw [Function.iterate_add_apply, Function.iterate_one, ind, ← nsmul_eq_mul, derivative_smul,
      nsmul_eq_mul, derivative_sum, Nat.factorial_succ, mul_comm (k + 1), Nat.cast_mul, mul_assoc]
    congr 1
    calc
      ∑ T ∈ S.powersetCard (#S - k), derivative (∏ a ∈ T, (X - C a)) =
      ∑ T ∈ S.powersetCard (#S - k), ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
        congr! with T hT
        simp_rw [derivative_prod_finset, derivative_X_sub_C, mul_one]
      _ = ∑ (T ∈ S.powersetCard (#S - k)) (i ∈ S) with i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
        rw [← sum_finset_product']
        grind
      _ = ∑ (T ∈ S.powersetCard (#S - (k + 1))) (i ∈ S) with i ∉ T, ∏ a ∈ T, (X - C a) := by
        apply sum_bij' (fun ⟨T, i⟩ _ => ⟨T.erase i, i⟩) (fun ⟨T, i⟩ _ => ⟨insert i T, i⟩)
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        all_goals grind
      _ = ∑ T ∈ S.powersetCard (#S - (k + 1)), ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a) := by
        rw [← sum_finset_product']
        grind
      _ = (k + 1) * ∑ T ∈ S.powersetCard (#S - (k + 1)), ∏ a ∈ T, (X - C a) := by
        rw [mul_sum]
        congr! 1 with T hT
        simp [sum_const, show #(S \ T) = k + 1 by grind]
      _ = _ := by grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inl.refine_1.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ c ∈ {r | IsUnit r ∨ Prime r}

Tactic:
left; exact ha₁

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
hc : IsRelPrime a b
x : α
hxa : x ∈ normalizedFactors a
hxb : x ∈ normalizedFactors b
x_dvd_a : x ∣ a
⊢ False

Tactic:
have x_dvd_b := dvd_of_mem_normalizedFactors hxb

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
hc : IsRelPrime a b
x : α
hxa : x ∈ normalizedFactors a
hxb : x ∈ normalizedFactors b
x_dvd_a : x ∣ a
x_dvd_b : x ∣ b
⊢ False
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case succ.mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬p.coeff a = 0 → ∃ a_2, ¬p.coeff a_2 = 0 ∧ a_2.succ = a + 1

Tactic:
intro h
      use a

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.content = 0 ↔ p = 0

Tactic:
by
  rw [content, Finset.gcd_eq_zero_iff]
  constructor <;> intro h
  · ext n
    simp_all
  · intro x
    simp [h]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬eval t g = 0
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
⊢ ¬↑m * eval t g = 0

Tactic:
mul_left_mem_nonZeroDivisors_eq_zero_iff hnzd

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬eval t g = 0
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
⊢ ¬eval t g = 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
p : R[X]
hp : p.Monic
⊢ normalize p = p

Tactic:
simp only [Polynomial.coe_normUnit, normalize_apply, hp.leadingCoeff, normUnit_one,
    Units.val_one, Polynomial.C.map_one, mul_one]

Goal state after:
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)
k : ℕ
a✝ : Nontrivial α
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count ↑(factors' a0)
p : { a // Irreducible a }
⊢ k ∣ Multiset.count p (factors' a0)

Tactic:
have pp : p = ⟨p.val, p.2⟩ := by simp only [Subtype.coe_eta]

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
k : ℕ
a✝ : Nontrivial α
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count ↑(factors' a0)
p : { a // Irreducible a }
pp : p = ⟨↑p, ⋯⟩
⊢ k ∣ Multiset.count p (factors' a0)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h : a * b = c ^ k
a✝ : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
⊢ k ∣ p.count (c ^ k).factors

Tactic:
apply dvd_count_pow _ hp

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h : a * b = c ^ k
a✝ : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
⊢ c ≠ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
⊢ a = p ^ Nat.find ⋯

Tactic:
by
  classical rw [count_factors_eq_find_of_dvd_pow hp, ← eq_pow_count_factors_of_dvd_pow hp h]
  exact h

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
x : K
⊢ IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x

Tactic:
by_cases hx : x = 0
  · simp [hx]
  let := invertibleOfNonzero hx
  exact IsAlgebraic.invOf_iff (R := R) (x := x)

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι✝ : Type u_1
inst✝¹ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h✝ : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit f i)
x✝¹ x✝ : ↑(Iio i)
h : ↑x✝¹ ≤ ↑x✝
⊢ (fun l ↦ (equiv l) (↑t l)) x✝¹ = piLTProj h ((fun l ↦ (equiv l) (↑t l)) x✝)

Tactic:
by simp_rw [← t.2 h]; apply nat

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
z : P ⊗[R] Q
⊢ ∃ a, (rTensor Q g) a = z

Tactic:
induction z with
  | zero => exact ⟨0, map_zero _⟩
  | tmul p q =>
    obtain ⟨n, rfl⟩ := hg p
    exact ⟨n ⊗ₜ[R] q, rfl⟩
  | add x y hx hy =>
    obtain ⟨x, rfl⟩ := hx
    obtain ⟨y, rfl⟩ := hy
    exact ⟨x + y, map_add _ _ _⟩

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

Goal state before:
pp: case add
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
x y : M ⊗[R] N
hx : ∃ S, x = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) S).sum
hy : ∃ S, y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) S).sum
⊢ ∃ S, x + y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) S).sum

Tactic:
obtain ⟨Sx, hx⟩ := hx

Goal state after:
case add
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
x y : M ⊗[R] N
hy : ∃ S, y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) S).sum
Sx : Multiset (M × N)
hx : x = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sx).sum
⊢ ∃ S, x + y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) S).sum