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

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
⊢ q ∈ b.primeFactorsList → False

Tactic:
hqb

Goal state after:
a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
hqb : q ∈ b.primeFactorsList
⊢ False
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
h : IsUnit ↑n
⊢ n = 1

Tactic:
← Nat.mod_zero n,

Goal state after:
n : ℕ
h : IsUnit ↑n
⊢ n % 0 = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
⊢ ringChar (ZMod n) = n

Tactic:
by
  rw [ringChar.eq_iff]
  exact ZMod.charP n

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.index = 0 ↔ Infinite (G ⧸ H)

Tactic:
simp [index_eq_card, Nat.card_eq_zero]

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

Goal state before:
pp: a : ℤ
b : ℕ
⊢ ↑a = 0 ↔ ↑b ∣ a

Tactic:
rw [← Int.cast_zero, ZMod.intCast_eq_intCast_iff, Int.modEq_zero_iff_dvd]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (toAddSubgroup H).FiniteIndex ↔ H.FiniteIndex

Tactic:
by
  simp [finiteIndex_iff, AddSubgroup.finiteIndex_iff]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_3
inst✝ : AddGroup G
H : AddSubgroup G
⊢ (AddSubgroup.toSubgroup H).FiniteIndex ↔ H.FiniteIndex

Tactic:
by
  simp [finiteIndex_iff, AddSubgroup.finiteIndex_iff]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ 1 ∈ n.properDivisors ↔ 1 < n

Tactic:
by
  rw [mem_properDivisors, and_iff_right (one_dvd _)]

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

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
⊢ ↑(↑a.val * a.val.gcdA n.succ + ↑n.succ * a.val.gcdB n.succ) = ↑(a.val.gcd n.succ)

Tactic:
by rw [← Nat.gcd_eq_gcd_ab a.val n.succ]; rfl

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

Goal state before:
pp: case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
h : Odd 0
⊢ 0 < ∑ i ∈ range 0, x ^ i

Tactic:
exact (Nat.not_odd_zero h).elim

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

Goal state before:
pp: a b n : ℕ
⊢ (b - 1) * ∑ i ∈ range n.succ, a / b ^ i =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)

Tactic:
rw [Nat.sub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero,
        Nat.div_one]

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

Goal state before:
pp: case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ (∑ i ∈ range 0, a / b ^ i) * (b - 1) ≤ a * b

Tactic:
sum_range_zero,

Goal state after:
case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 * (b - 1) ≤ a * b
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.mpr
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a = 0 ∨ 2 * a.val = n✝ + 1 → n✝ + 1 ∣ 2 * a.val

Tactic:
· rintro (rfl | h)
    · rw [val_zero, mul_zero]
      apply dvd_zero
    · rw [h]

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

Goal state before:
pp: n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * (n * n.centralBinom) ≤ 2 * (2 * n + 1) * n.centralBinom

Tactic:
rw [← mul_assoc]

Goal state after:
n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * n * n.centralBinom ≤ 2 * (2 * n + 1) * n.centralBinom
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n m : ℕ
nzm : NeZero (m + 1)
a : ZMod (m + 1)
h : a.val < n
⊢ ?m.35 ≠ 0

Tactic:
rintro (rfl : n = 0); simp at h

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

Goal state before:
pp: x : ℕ
hx : x.succ ≠ 0
b : ℕ
hxb : x.succ < b + succ 1
⊢ [(x + 1) % (b + 2)] = [x.succ]

Tactic:
mod_eq_of_lt hxb

Goal state after:
x : ℕ
hx : x.succ ≠ 0
b : ℕ
hxb : x.succ < b + succ 1
⊢ [x.succ] = [x.succ]
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : NonAssocRing R
n✝ : ℕ
f : R →+* ZMod (n✝ + 1)
k : ZMod (n✝ + 1)
⊢ f k.cast = k

Tactic:
dsimp [ZMod.cast]
    rw [map_natCast, natCast_zmod_val]

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

Goal state before:
pp: case nil
b : ℕ
hb : 1 < b
L2 : List ℕ
len : [].length = L2.length
w1 : ∀ l ∈ [], l < b
w2 : ∀ l ∈ L2, l < b
h : ofDigits b [] = ofDigits b L2
⊢ [] = L2

Tactic:
simp only [List.length_nil] at len

Goal state after:
case nil
b : ℕ
hb : 1 < b
L2 : List ℕ
len : 0 = L2.length
w1 : ∀ l ∈ [], l < b
w2 : ∀ l ∈ L2, l < b
h : ofDigits b [] = ofDigits b L2
⊢ [] = L2
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p n : ℕ
⊢ n.divMaxPow p * p ^ padicValNat p n = n

Tactic:
divMaxPow_mul_pow_padicValNat

Goal state after:
p n : ℕ
⊢ n = n
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
⊢ emultiplicity a b < ↑k ↔ ¬a ^ k ∣ b

Tactic:
pow_dvd_iff_le_emultiplicity,

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
⊢ emultiplicity a b < ↑k ↔ ¬↑k ≤ emultiplicity a b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hdvd : a ∣ b
⊢ multiplicity a b ≠ 0

Tactic:
by simpa [multiplicity_eq_zero]

Goal state after:
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
  rw [sub_eq_add_neg, emultiplicity_add_of_gt] <;> rw [emultiplicity_neg]; assumption

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
y : G
α : Type u_6
inst✝ : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : y ^ k ∈ zpowers y
⊢ (MulAction.toPerm (y ^ k)) a = a

Tactic:
← MulAction.toPermHom_apply,

Goal state after:
G : Type u_1
inst✝¹ : Group G
y : G
α : Type u_6
inst✝ : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : y ^ k ∈ zpowers y
⊢ ((MulAction.toPermHom G α) (y ^ k)) a = a
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
x : G
hx : x⁻¹ ∈ s
⊢ x ∈ powers x⁻¹

Tactic:
simp [(hs _ hx).mem_powers_iff_mem_zpowers]

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

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

Tactic:
rw [← ENat.natCast_inj, ← (Nat.finiteMultiplicity_iff.2
      ⟨hp.ne_one, (p ^ n).factorial_pos⟩).emultiplicity_eq_multiplicity]
  induction n with
  | zero => simp [hp.emultiplicity_one]
  | succ n h =>
    rw [pow_succ', hp.emultiplicity_factorial_mul, h, Finset.sum_range_succ, ENat.natCast_add]

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

Goal state after:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n < p ^ b
i : ℕ
⊢ i ∈ {i ∈ Ico 1 n | p ^ i ∣ n} ↔ i ∈ {i ∈ Ico 1 b | p ^ i ∣ n}
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: 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
l : ℤ
hl : x ^ (k * l) = x ^ 1
h1 : k * l = 1
⊢ x = x ^ k ∨ x⁻¹ = x ^ k

Tactic:
rcases (Int.mul_eq_one_iff_eq_one_or_neg_one).mp h1 with (h | h) <;> simp [h.1]

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

Goal state before:
pp: case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b) → a = b

Tactic:
intro h
    refine eq_of_factorization_eq ha hb fun p => ?_
    by_cases pp : p.Prime
    · simp [factorization_def, pp, h p pp]
    · simp [factorization_eq_zero_of_not_prime, pp]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_6
inst✝ : Group G
x : G
h : Infinite G
⊢ orderOf x ∣ Nat.card G

Tactic:
· simp only [card_eq_zero_of_infinite, dvd_zero]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
hn : 0 < n
g g' : R[X]
H : (expand R n) g = (expand R n) g'
k : ℕ
⊢ g.coeff k = g'.coeff k

Tactic:
rw [← coeff_expand_mul hn, H, coeff_expand_mul hn]

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

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : r ≠ 0
this : r.natDegree = 0
⊢ p * r = p * C (p * r).leadingCoeff

Tactic:
rw [eq_C_of_natDegree_eq_zero this]

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : r ≠ 0
this : r.natDegree = 0
⊢ p * C (r.coeff 0) = p * C (p * C (r.coeff 0)).leadingCoeff
Module: Mathlib.Algebra.Polynomial.RingDivision

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

Tactic:
exact h.val_inv_mul

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

Goal state before:
pp: case prime
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hprime : Nat.Prime p
hchar : CharP R p
this : Fact (CharP R p)
⊢ (expand R p) (contract p f) = f

Tactic:
exact expand_contract p hf hprime.ne_zero

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]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k)) f) = f ^ p ^ k
| f ^ p ^ (k + 1)

Tactic:
rw [pow_succ, pow_mul, ← n_ih]

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k)) f) = f ^ p ^ k
| map (iterateFrobenius R p k) ((expand R (p ^ k)) f) ^ p
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
rw [zero_mul, C_0, zero_mul]

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

Goal state before:
pp: case neg.a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : ¬C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
⊢ (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree ≤ q.natDegree

Tactic:
compute_degree!
    rwa [Nat.sub_add_cancel]

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = q.natDegree
⊢ p.leadingCoeff * q.coeff (q.natDegree - p.natDegree + p.natDegree) + -(q.leadingCoeff * p.coeff p.natDegree) = 0

Tactic:
tsub_add_cancel_of_le h,

Goal state after:
case a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = q.natDegree
⊢ p.leadingCoeff * q.coeff q.natDegree + -(q.leadingCoeff * p.coeff p.natDegree) = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
n : ℕ
hn : q.degree ≤ ↑n
⊢ ∑ i, (monomial ↑i) ((p %ₘ q).coeff ↑i) = p %ₘ q

Tactic:
nontriviality R
  exact
    (sum_fin (fun i c => monomial i c) (by simp) ((degree_modByMonic_lt _ hq).trans_le hn)).trans
      (sum_monomial_eq _)

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = q.natDegree
⊢ q.leadingCoeff * p.leadingCoeff + -(q.leadingCoeff * p.leadingCoeff) = 0

Tactic:
add_neg_cancel

Goal state after:
case a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = q.natDegree
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr
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
⊢ (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i

Tactic:
refine Nat.decreasingInduction' (fun n hn _ ih ↦ ?_) (le_of_not_ge h) ?_
    · rw [coeff_divByMonic_X_sub_C_rec, ih, eq_comm, Icc_eq_cons_Ioc (Nat.succ_le_iff.mpr hn),
          sum_cons, Nat.sub_self, pow_zero, one_mul, mul_sum]
      congr 1; refine sum_congr ?_ fun i hi ↦ ?_
      · ext; simp
      rw [← mul_assoc, ← pow_succ', eq_comm, i.sub_succ', Nat.sub_add_cancel]
      apply Nat.le_sub_of_add_le
      rw [add_comm]; exact (mem_Icc.mp hi).1
    · exact this _ le_rfl

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : ∀ (n : ℕ), (derivative p).coeff n = coeff 0 n
hp' : p ≠ 0
f_nat_degree_pos : 0 < p.natDegree
m : ℕ := p.natDegree - 1
hm : m + 1 = p.natDegree
h2 : p = 0
⊢ False

Tactic:
exact hp' h2

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

Goal state before:
pp: ι : Type u_4
α : ι → Type u_5
f : (i : ι) → Filter (α i)
⊢ (pi f).ker = univ.pi fun i ↦ (f i).ker

Tactic:
simp [Set.pi_def, Filter.pi]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
f : α → β
l : Filter β
inst✝ : l.IsCountablyGenerated
h : Tendsto f cofinite l
⊢ (f ⁻¹' l.ker)ᶜ.Countable

Tactic:
← ker_comap

Goal state after:
α : Type u_2
β : Type u_3
f : α → β
l : Filter β
inst✝ : l.IsCountablyGenerated
h : Tendsto f cofinite l
⊢ (comap f l).kerᶜ.Countable
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ ∅ ∈ f ×ˢ g ↔ ∅ ∈ f ∨ ∅ ∈ g

Tactic:
mem_prod_iff,

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ ∅) ↔ ∅ ∈ f ∨ ∅ ∈ g
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type ?u.3
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ Associated (gcd a b * lcm a b) (a * b)

Tactic:
EuclideanDomain.gcd_mul_lcm

Goal state after:
R : Type ?u.3
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ Associated (a * b) (a * b)
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inr.inl
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₂ : Prime c✝
c : M₀
hc : x = c✝ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
rw [hc]; rw [hc, mul_assoc] at hprod
        refine Submonoid.mul_mem _ (subset_closure ?_)
          (hind _ _ ?_ hs (mul_left_cancel₀ ha₂.ne_zero hprod))
        · right; exact ha₂
        rw [← mul_left_cancel₀ ha₂.ne_zero hprod]
        exact multiset_prod_mem _ _ (fun t ht => subset_closure (hs t ht))

Goal state after:
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:
by rwa [add_tsub_cancel_of_le h] at this

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
x : σ →₀ M
⊢ degree (mapDomain f x) = degree x

Tactic:
simp [mapDomain, sum]
  dsimp [degree_apply]

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
⊢ (p / q).degree < p.degree

Tactic:
have hq0 : q ≠ 0 := fun hq0 => by simp [hq0] at hq

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
hq0 : q ≠ 0
⊢ (p / q).degree < p.degree
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a b : FactorSet α
h : a.prod ≤ b.prod
⊢ a ≤ b

Tactic:
have : a.prod.factors ≤ b.prod.factors := factors_mono h

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a b : FactorSet α
h : a.prod ≤ b.prod
this : a.prod.factors ≤ b.prod.factors
⊢ a ≤ b
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
⊢ IsUnit (EuclideanDomain.gcd (map f p) (map f q)) ↔ IsUnit (EuclideanDomain.gcd p q)

Tactic:
gcd_map,

Goal state after:
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
⊢ IsUnit (map f (EuclideanDomain.gcd p q)) ↔ IsUnit (EuclideanDomain.gcd p q)
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f : R[X]
⊢ WellFounded DvdNotUnit

Tactic:
classical
      refine
        RelHomClass.wellFounded
          (⟨fun p : R[X] =>
              ((if p = 0 then ⊤ else ↑p.degree : WithTop (WithBot ℕ)), p.leadingCoeff), ?_⟩ :
            DvdNotUnit →r Prod.Lex (· < ·) DvdNotUnit)
          (wellFounded_lt.prod_lex ‹WfDvdMonoid R›.wf)
      rintro a b ⟨ane0, ⟨c, ⟨not_unit_c, rfl⟩⟩⟩
      rw [Polynomial.degree_mul, if_neg ane0]
      split_ifs with hac
      · rw [hac, Polynomial.leadingCoeff_zero]
        apply Prod.Lex.left
        exact WithTop.coe_lt_top _
      have cne0 : c ≠ 0 := right_ne_zero_of_mul hac
      simp only [Polynomial.leadingCoeff_mul]
      by_cases hdeg : c.degree = (0 : ℕ)
      · simp only [hdeg, Nat.cast_zero, add_zero]
        refine Prod.Lex.right _ ⟨?_, ⟨c.leadingCoeff, fun unit_c => not_unit_c ?_, rfl⟩⟩
        · rwa [Ne, Polynomial.leadingCoeff_eq_zero]
        rw [Polynomial.isUnit_iff, Polynomial.eq_C_of_degree_eq_zero hdeg]
        use c.leadingCoeff, unit_c
        rw [Polynomial.leadingCoeff, Polynomial.natDegree_eq_of_degree_eq_some hdeg]
      · apply Prod.Lex.left
        rw [Polynomial.degree_eq_natDegree cne0] at *
        simp only [Nat.cast_inj] at hdeg
        rw [WithTop.coe_lt_coe, Polynomial.degree_eq_natDegree ane0, ← Nat.cast_add, Nat.cast_lt]
        exact lt_add_of_pos_right _ (Nat.pos_of_ne_zero hdeg)

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ Irreducible (p * C p.leadingCoeff⁻¹) ↔ ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q

Tactic:
(monic_mul_leadingCoeff_inv hp0).irreducible_iff_degree_lt

Goal state after:
R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ (∀ (q : R[X]), q.degree ≤ ↑((p * C p.leadingCoeff⁻¹).natDegree / 2) → q ∣ p * C p.leadingCoeff⁻¹ → IsUnit q) ↔
    ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q

R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ p * C p.leadingCoeff⁻¹ ≠ 1
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
s t : Set (σ →₀ ℕ)
⊢ s + t ⊆ (fun x ↦ (monomial x) 1) ⁻¹' ↑(restrictSupport R s * restrictSupport R t)

Tactic:
Set.add_subset_iff

Goal state after:
case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
s t : Set (σ →₀ ℕ)
⊢ ∀ x ∈ s, ∀ y ∈ t, x + y ∈ (fun x ↦ (monomial x) 1) ⁻¹' ↑(restrictSupport R s * restrictSupport R t)
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
h : P → N
hgh : RightInverse h ⇑g
z : Q ⊗[R] P
⊢ (toFun Q hfg) ((inverse_of_rightInverse Q hfg hgh) z) = z

Tactic:
obtain ⟨y, rfl⟩ := lTensor_surjective Q (hgh.surjective) z

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
h : P → N
hgh : RightInverse h ⇑g
y : Q ⊗[R] N
⊢ (toFun Q hfg) ((inverse_of_rightInverse Q hfg hgh) ((lTensor Q g) y)) = (lTensor Q g) y
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 A
⊢ Submodule.restrictScalars R (map includeLeft I) = (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype).range

Tactic:
rw [← SetLike.coe_set_eq]

Goal state after:
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 A
⊢ ↑(Submodule.restrictScalars R (map includeLeft I)) =
    ↑(LinearMap.rTensor B (Submodule.restrictScalars R I).subtype).range
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

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

Tactic:
induction x with

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

Goal state before:
pp: 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 : M ⊗[R] N
⊢ ∃ S, x = S.sum fun m n ↦ m ⊗ₜ[R] n

Tactic:
induction x with

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

Goal state before:
pp: case a.refine_4.tmul
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 A
x✝ : A ⊗[R] B
hx : x✝ ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)))
x : ↥(Submodule.restrictScalars R I) ⊗[R] B
a : A
b : B
⊢ ∃ y,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y =
      a ⊗ₜ[R] b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x

Tactic:
induction x with

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
⊢ Submodule.restrictScalars R (map includeRight I) = (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype).range

Tactic:
rw [← SetLike.coe_set_eq]

Goal state after:
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
⊢ ↑(Submodule.restrictScalars R (map includeRight I)) =
    ↑(LinearMap.lTensor A (Submodule.restrictScalars R I).subtype).range