mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ.succ
n✝ : ℕ
⊢ ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1 ↔ Prime (n✝ + 1 + 1)

Tactic:
rw [← properDivisors_eq_singleton_one_iff_prime]
      refine ⟨fun h => ?_, fun h => h.symm ▸ sum_singleton _ _⟩
      rw [@eq_comm (Finset ℕ) _ _]
      apply
        eq_properDivisors_of_subset_of_sum_eq_sum
          (singleton_subset_iff.2
            (one_mem_properDivisors_iff_one_lt.2 (succ_lt_succ (Nat.succ_pos _))))
          ((sum_singleton _ _).trans h.symm)

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (-a + a).val = (n - a.val + a.val) % n

Tactic:
neg_add_cancel,

Goal state after:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ val 0 = (n - a.val + a.val) % n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n : ℕ
inst✝ : Fact (1 < n)
a : ZMod n
m : ℕ
ih : (a ^ m).val ≤ a.val ^ m
⊢ (a ^ m * a).val ≤ a.val ^ (m + 1)

Tactic:
pow_succ

Goal state after:
case succ
n : ℕ
inst✝ : Fact (1 < n)
a : ZMod n
m : ℕ
ih : (a ^ m).val ≤ a.val ^ m
⊢ (a ^ m * a).val ≤ a.val ^ m * a.val
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p : ℕ
hp : p ≠ 0
⊢ p.divMaxPow p = 1

Tactic:
by
  simpa using divMaxPow_base_pow hp 1

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

Goal state before:
pp: case e'_3
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
this : 0 < l.getLast hl
⊢ (b + 2) ^ (l.length - 1) = (b + 2) ^ (l.length - 1) * succ 0

Tactic:
rw [Nat.mul_one]

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

Goal state before:
pp: case cons
b hd : ℕ
tl : List ℕ
IH : (∀ x ∈ tl, x < b + 2) → ofDigits (b + 2) tl < (b + 2) ^ tl.length
hl : ∀ x ∈ hd :: tl, x < b + 2
⊢ ↑hd + (b + 2) * ofDigits (b + 2) tl < (b + 2) ^ (tl.length + 1)

Tactic:
pow_succ

Goal state after:
case cons
b hd : ℕ
tl : List ℕ
IH : (∀ x ∈ tl, x < b + 2) → ofDigits (b + 2) tl < (b + 2) ^ tl.length
hl : ∀ x ∈ hd :: tl, x < b + 2
⊢ ↑hd + (b + 2) * ofDigits (b + 2) tl < (b + 2) ^ tl.length * (b + 2)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case succ.isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
h✝ : FiniteMultiplicity a b
hk : ↑(n✝ + 1) ≤ ↑(Nat.find h✝)
⊢ a ^ (n✝ + 1) ∣ b

Tactic:
norm_cast at hk
    simpa using (Nat.find_min _ (lt_of_succ_le hk))

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
h_1 : FiniteMultiplicity a b
⊢ ↑(Nat.find h_1) ≤ if h : FiniteMultiplicity c d then ↑(Nat.find h) else ⊤

Tactic:
obtain ⟨w, h_1⟩ := h_1
      split
      next h_2 =>
        simp_all only [cast_le, le_find_iff, lt_find_iff, Decidable.not_not, le_refl,
          not_true_eq_false, not_false_eq_true, implies_true]
      next h_2 => simp_all only [not_exists, Decidable.not_not, le_top]

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ (b.digits (ofDigits b L)).sum = L.sum

Tactic:
nth_rewrite 2 [← (setInvOn_digitsAppend_ofDigits hb l).1 hL]

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ (b.digits (ofDigits b L)).sum = (b.digitsAppend l (ofDigits b L)).sum
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
hfin : FiniteMultiplicity a a
⊢ emultiplicity a a = 1

Tactic:
simp [hfin.emultiplicity_eq_multiplicity]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
⊢ a.minFac ∣ n

Tactic:
obtain ⟨b, hb⟩ : ∃ b : ℕ, a = b * a.minFac := exists_eq_mul_left_of_dvd a.minFac_dvd

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
b : ℕ
hb : a = b * a.minFac
⊢ a.minFac ∣ n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : (p * i + r).factorization p = 0
⊢ ¬p ∣ r

Tactic:
rw [factorization_eq_zero_iff] at h

Goal state after:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : ¬Prime p ∨ ¬p ∣ p * i + r ∨ p * i + r = 0
⊢ ¬p ∣ r
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case refine_1
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p ∣ p * i + r

Tactic:
rwa [← Nat.dvd_add_iff_right (dvd_mul_right p i)]

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

Goal state before:
pp: a b p : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)

Tactic:
simp only [ordProj_mul p ha hb]
  rw [div_mul_div_comm (ordProj_dvd a p) (ordProj_dvd b p)]

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : b ∣ a
⊢ b ≤ a

Tactic:
exact le_of_dvd ha.bot_lt hab

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
x✝ : ∃ m, x ^ p ^ m = 1
w✝ : ℕ
hm : x ^ p ^ w✝ = 1
⊢ ∃ k, orderOf x = p ^ k

Tactic:
by
    obtain ⟨k, _, hk⟩ := (Nat.dvd_prime_pow hp.elim).mp (orderOf_dvd_of_pow_eq_one hm)
    exact ⟨k, hk⟩

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

Goal state before:
pp: case neg
p n k : ℕ
h : n < p
hnk : k ≤ n
⊢ (n !.factorization - (k ! * (n - k)!).factorization) p = 0

Tactic:
Finsupp.coe_tsub,

Goal state after:
case neg
p n k : ℕ
h : n < p
hnk : k ≤ n
⊢ (⇑n !.factorization - ⇑(k ! * (n - k)!).factorization) p = 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
⊢ {y | ¬IsOfFinOrder y}.Infinite

Tactic:
by
  let s := { n | 0 < n }.image fun n : ℕ => x ^ n
  have hs : s ⊆ { y : G | ¬IsOfFinOrder y } := by
    rintro - ⟨n, hn : 0 < n, rfl⟩ (contra : IsOfFinOrder (x ^ n))
    apply h
    rw [isOfFinOrder_iff_pow_eq_one] at contra ⊢
    obtain ⟨m, hm, hm'⟩ := contra
    exact ⟨n * m, mul_pos hn hm, by rwa [pow_mul]⟩
  suffices s.Infinite by exact this.mono hs
  contrapose! h
  have : ¬Injective fun n : ℕ => x ^ n := by
    have := Set.not_injOn_infinite_finite_image (Set.Ioi_infinite 0) h
    contrapose this
    exact Set.injOn_of_injective this
  rwa [injective_pow_iff_not_isOfFinOrder, Classical.not_not] at this

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : ℕ
hR : ExpChar R p
⊢ (-1 + 1) ^ p = 0

Tactic:
neg_add_cancel,

Goal state after:
R : Type u_1
inst✝ : Ring R
p : ℕ
hR : ExpChar R p
⊢ 0 ^ p = 0
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p n : ℕ
hR : ExpChar R p
⊢ (-1 + 1) ^ p ^ n = 0

Tactic:
neg_add_cancel,

Goal state after:
R : Type u_1
inst✝ : Ring R
p n : ℕ
hR : ExpChar R p
⊢ 0 ^ p ^ n = 0
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case succ
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
p : ℕ
pp : Prime (p + 1)
hb : n < (p + 1) ^ b
h1 : (p + 1) ^ i ∣ n
⊢ i < b

Tactic:
← Nat.pow_lt_pow_iff_right (Prime.one_lt pp)

Goal state after:
case succ
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
p : ℕ
pp : Prime (p + 1)
hb : n < (p + 1) ^ b
h1 : (p + 1) ^ i ∣ n
⊢ (p + 1) ^ i < (p + 1) ^ b
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: h2 : _root_.Prime 2
⊢ ∀ {n : ℕ}, n ≠ 0 → emultiplicity 2 n ! < ↑n

Tactic:
refine binaryRec ?_ ?_

Goal state after:
case refine_1
h2 : _root_.Prime 2
⊢ 0 ≠ 0 → emultiplicity 2 0! < ↑0

case refine_2
h2 : _root_.Prime 2
⊢ ∀ (b : Bool) (n : ℕ), (n ≠ 0 → emultiplicity 2 n ! < ↑n) → bit b n ≠ 0 → emultiplicity 2 (bit b n)! < ↑(bit b n)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n : ℕ
⊢ _root_.Pairwise (Function.onFun Coprime fun p ↦ ↑p ^ n.factorization ↑p)

Tactic:
intro p1 p2 hp
  refine Nat.Coprime.pow (n.factorization p1) (n.factorization p2) ?_
  refine (Nat.coprime_primes ?_ ?_).mpr <| Subtype.coe_ne_coe.mpr hp
  · exact Nat.prime_of_mem_primeFactors p1.2
  · exact Nat.prime_of_mem_primeFactors p2.2

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case succ
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝¹ : LeftCancelMonoid M
inst✝ : Finite M
S : Set M
hS1 : S.Nonempty
hS2 : S * S = S
a : M
ha : a ∈ S
n : ℕ
ih : a ^ (n + 1) ∈ S
⊢ a ^ (n + 1 + 1) ∈ S * S

Tactic:
pow_succ

Goal state after:
case succ
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝¹ : LeftCancelMonoid M
inst✝ : Finite M
S : Set M
hS1 : S.Nonempty
hS2 : S * S = S
a : M
ha : a ∈ S
n : ℕ
ih : a ^ (n + 1) ∈ S
⊢ a ^ (n + 1) * a ∈ S * S
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr.inr
G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
h : |(-1)| = 1
⊢ orderOf (-1) ≤ 2

Tactic:
exact orderOf_le_of_pow_eq_one zero_lt_two (by simp)

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
ih :
  (if hq : q.Monic then ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2
    else p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) =
    p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)
⊢ (have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
      have _wf := ⋯;
      have dm := (p - q * z).divModByMonicAux ⋯;
      (z + dm.1, dm.2)).2 =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0

Tactic:
dif_pos hq

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
ih :
  ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2 =
    p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)
⊢ (have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
      have _wf := ⋯;
      have dm := (p - q * z).divModByMonicAux ⋯;
      (z + dm.1, dm.2)).2 =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: 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
⊢ ↑t.card + 1 ≤ p.degree

Tactic:
rw [← degree_add_divByMonic (monic_X_sub_C x) hdeg, degree_X_sub_C, add_comm]
            exact add_le_add (le_refl (1 : WithBot ℕ)) htd

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this : Nontrivial R
⊢ ¬(p /ₘ (X - C a) ^ rootMultiplicity a p).IsRoot a

Tactic:
← dvd_iff_isRoot

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this : Nontrivial R
⊢ ¬X - C a ∣ p /ₘ (X - C a) ^ rootMultiplicity a p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) = p
⊢ False

Tactic:
rw [hq, ← mul_assoc, ← pow_succ, rootMultiplicity_eq_multiplicity, if_neg hp] at this

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ (multiplicity (X - C a) p + 1) * q = p
⊢ False
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
I_fin : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
hU : ⋂ i, V i ⊆ U
⊢ U ∈ ⨅ i, s i

Tactic:
have := I_fin.fintype

Goal state after:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
I_fin : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
hU : ⋂ i, V i ⊆ U
this : Fintype ↑I
⊢ U ∈ ⨅ i, s i
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α : Type u_1
f : Filter α
⊢ f.IsCountablyGenerated ↔ ∃ x, f.HasAntitoneBasis x

Tactic:
by
  constructor
  · intro h
    exact f.exists_antitone_basis
  · rintro ⟨x, h⟩
    rw [h.1.eq_iInf]
    exact isCountablyGenerated_seq x

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
⊢ (-p + p) %ₘ q = 0

Tactic:
neg_add_cancel,

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
⊢ 0 %ₘ q = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case zero
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
h : ∀ m < 0, (X - C a) ^ (m + 1) ∣ p
⊢ (X - C a) ^ 0 ∣ p

pp: case succ
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
h : ∀ m < n + 1, (X - C a) ^ (m + 1) ∣ p
⊢ (X - C a) ^ (n + 1) ∣ p

Tactic:
· rw [pow_zero]
    apply one_dvd

Goal state after:
case succ
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
h : ∀ m < n + 1, (X - C a) ^ (m + 1) ∣ p
⊢ (X - C a) ^ (n + 1) ∣ p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ rootMultiplicity a p ≤ n ↔ ¬(X - C a) ^ (n + 1) ∣ p

Tactic:
by
  rw [← (le_rootMultiplicity_iff p0).not, not_le, Nat.lt_add_one_iff]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
a : R
hzero : p + q ≠ 0
⊢ min (rootMultiplicity a p) (rootMultiplicity a q) ≤ rootMultiplicity a (p + q)

Tactic:
rw [le_rootMultiplicity_iff hzero]
  exact min_pow_dvd_add (pow_rootMultiplicity_dvd p a) (pow_rootMultiplicity_dvd q a)

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

Goal state before:
pp: case refine_2
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ (∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x) → t ∈ ⨅ x, f ↑x

Tactic:
· rintro ⟨p, hpf, rfl⟩
    exact iInter_mem.2 fun a => mem_iInf_of_mem a (hpf a a.2)

Goal state after:
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
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
have : { y | ¬x ≤ f y }.Finite := Filter.eventually_cofinite.mp (tendsto_atTop.1 hf 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
y : α
hys : y ∈ s
x : β
hx : f y < x
this : {y | ¬x ≤ f y}.Finite
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
f' : Filter α
g' : Filter β
⊢ Disjoint (f ×ˢ g) (f' ×ˢ g') ↔ Disjoint f f' ∨ Disjoint g g'

Tactic:
by
  simp only [disjoint_iff, prod_inf_prod, prod_eq_bot]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ ∀ x ∈ normalizedFactors a, Prime x

Tactic:
by
  rw [normalizedFactors, factors]
  split_ifs with ane0; · simp
  intro x hx; rcases Multiset.mem_map.1 hx with ⟨y, ⟨hy, rfl⟩⟩
  rw [(normalize_associated _).prime_iff]
  exact (Classical.choose_spec (UniqueFactorizationMonoid.exists_prime_factors a ane0)).1 y hy

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

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h✝ : Nontrivial α
⊢ normalizedFactors m.prod = m

Tactic:
· simpa only [← Multiset.rel_eq, ← associated_eq_eq] using
      prime_factors_unique prime_of_normalized_factor h
        (prod_normalizedFactors (m.prod_ne_zero_of_prime h))

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
⊢ q.prod = (p + factors c).prod

Tactic:
rw [eqc, Multiset.prod_add]
    congr
    refine associated_iff_eq.mp (factors_prod fun hc => ?_).symm
    refine not_irreducible_zero (hq _ ?_)
    rw [← prod_eq_zero_iff, eqc, hc, mul_zero]

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

Goal state before:
pp: T : Type w
inst✝⁵ : CommRing T
p : T[X]
S : Type u_1
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : S
⊢ a ∈ p.rootSet S ↔ p ≠ 0 ∧ (aeval a) p = 0

Tactic:
rw [mem_rootSet', Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective T S)]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
s : Multiset R
⊢ (Multiset.map (fun a ↦ X - C a) s).prod ∣ p ↔ s ≤ p.roots

Tactic:
exact
  ⟨fun h =>
    Multiset.le_iff_count.2 fun r => by
      rw [count_roots, le_rootMultiplicity_iff hp, ← Multiset.prod_replicate, ←
        Multiset.map_replicate fun a => X - C a, ← Multiset.filter_eq]
      exact (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map <| s.filter_le _).trans h,
    fun h =>
    (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map h).trans p.prod_multiset_X_sub_C_dvd⟩

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
hdfg0 : derivative f * g ≠ 0
hr' : rootMultiplicity a f - 1 = rootMultiplicity a (f * r)
this : IsDomain R
⊢ False

Tactic:
rootMultiplicity_mul (hr ▸ hdfg0),

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
hdfg0 : derivative f * g ≠ 0
hr' : rootMultiplicity a f - 1 = rootMultiplicity a f + rootMultiplicity a r
this : IsDomain R
⊢ False
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 ≠ 0
⊢ 1 = C (p.coeff 0 * (p.coeff 0)⁻¹)

Tactic:
mul_inv_cancel₀ hc,

Goal state after:
R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 ≠ 0
⊢ 1 = C 1
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : a ≠ 0
⊢ (Associates.mk a).factors.prod = Associates.mk a

Tactic:
· simp [ha, prod_mk, mk_eq_mk_iff_associated, UniqueFactorizationMonoid.factors_prod]

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:
by
  have hq0 : q ≠ 0 := fun hq0 => by simp [hq0] at hq
  rw [div_def, mul_comm, degree_mul_leadingCoeff_inv _ hq0]
  exact degree_divByMonic_lt _ (q * C q.leadingCoeff⁻¹) hp
    (by rw [degree_mul_leadingCoeff_inv _ hq0]; exact hq)

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : c.degree = ↑0
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (↑a.degree, a.leadingCoeff)
    (↑(a.degree + c.degree), a.leadingCoeff * c.leadingCoeff)

Tactic:
simp only [hdeg, Nat.cast_zero, add_zero]

Goal state after:
case pos
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : c.degree = ↑0
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (↑a.degree, a.leadingCoeff) (↑a.degree, a.leadingCoeff * c.leadingCoeff)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
hp0 : IsUnit p.leadingCoeff
⊢ (normalize p).Monic

Tactic:
Monic,

Goal state after:
R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
hp0 : IsUnit p.leadingCoeff
⊢ (normalize p).leadingCoeff = 1
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 = (replicate k ↑⟨p, hp⟩).prod

Tactic:
Multiset.prod_replicate,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
k : ℕ
⊢ p ^ k = ↑⟨p, hp⟩ ^ k
Module: Mathlib.Algebra.Azumaya.Defs

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
this : Module (A ⊗[R] Aᵐᵒᵖ) A := Algebra.module
r : R
ab : A ⊗[R] Aᵐᵒᵖ
a : A
⊢ (r • ab) • a = r • ab • a

Tactic:
change TensorProduct.Algebra.moduleAux _ _ = _ • TensorProduct.Algebra.moduleAux _ _
      simp

Goal state after:
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:
by
  rw [← map_ratCast (algebraMap R A)]
  exact isAlgebraic_algebraMap (Rat.cast n)

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : DirectLimit F f → DirectLimit F f → Prop
ih : ∀ (i : ι) (x y : F i), C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧
x y : DirectLimit F f
⊢ C x y

Tactic:
obtain ⟨_, _, _, rfl, rfl⟩ := exists_eq_mk₂ f x y

Goal state after:
ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : DirectLimit F f → DirectLimit F f → Prop
ih : ∀ (i : ι) (x y : F i), C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧
w✝² : ι
w✝¹ w✝ : F w✝²
⊢ C ⟦⟨w✝², w✝¹⟩⟧ ⟦⟨w✝², w✝⟩⟧