mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ (liftSupQuotQuotMk I J).comp (quotQuotToQuotSup I J) = RingHom.id ((R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)

Tactic:
by
      repeat apply Ideal.Quotient.ringHom_ext
      rfl

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case refine_2
α : Type u_1
f : α → α
x : α
m✝ n✝ m n : ℕ
x✝ : 0 < m
ih : IsPeriodicPt f (n % m) x → IsPeriodicPt f m x → IsPeriodicPt f ((n % m).gcd m) x
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (m.gcd n) x

Tactic:
· rw [Nat.gcd_rec]
    exact ih (hn.mod hm) hm

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x y : α
n : ℕ
hx : IsPeriodicPt f n x
hy : IsPeriodicPt f n y
hn : 0 < n
h : f x = f y
⊢ x = y

Tactic:
by
  rw [← hx.eq, ← hy.eq, ← iterate_pred_comp_of_pos f hn, comp_apply, comp_apply, h]

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℕ
⊢ a ^ n • b = b ↔ minimalPeriod (fun x ↦ a • x) b ∣ n

Tactic:
by
  rw [← period_eq_minimalPeriod, pow_smul_eq_iff_period_dvd]

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
i : ι
⊢ minimalPeriod (f i) (x i) ∣ minimalPeriod (Pi.map f) x

Tactic:
simp only [minimalPeriod_piMap]
  by_cases h : {n | 0 < n ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}.Nonempty
  · exact (Nat.sInf_mem h).2 i
  · simp [not_nonempty_iff_eq_empty.mp h]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
g h k : G
a b c : α
hg : b = g • a
⊢ Subgroup.map (↑(MulAut.conj g)) (stabilizer G a) = stabilizer G b

Tactic:
rw [hg, stabilizer_smul_eq_stabilizer_map_conj g a, ← MulEquiv.toMonoidHom_eq_coe]

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.prev hs x hx ∈ s

Tactic:
← next_reverse_eq_prev,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.reverse.next ⋯ x ⋯ ∈ s
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: k n : ℕ
hk : k ≠ 0
⊢ (n ^ k).primeFactors = n.primeFactors

Tactic:
by
  cases k
  · simp at hk
  rw [primeFactors_pow_succ]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : Surjective ⇑f
⊢ (map f H).index ∣ H.index

Tactic:
rw [index_map, f.range_eq_top_of_surjective hf, index_top, mul_one]

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : Surjective ⇑f
⊢ (H ⊔ f.ker).index ∣ H.index
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (J ⊓ L).relIndex (K ⊓ L) ≠ 0

Tactic:
by
  rw [← range_subtype L, inf_comm, ← map_comap_eq, inf_comm, ← map_comap_eq, ← relIndex_comap,
    comap_map_eq_self_of_injective (subtype_injective L)]
  exact relIndex_comap_ne_zero _ hJK

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

Goal state before:
pp: case succ
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).cast = if ↑(n + 1) ≤ a.cast + b.cast then a.cast + b.cast - ↑(n + 1) else a.cast + b.cast

Tactic:
change Fin (n + 1) at a b

Goal state after:
case succ
n : ℕ
a b : Fin (n + 1)
⊢ (a + b).cast = if ↑(n + 1) ≤ cast a + cast b then cast a + cast b - ↑(n + 1) else cast a + cast b
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
f : ι → Subgroup G
⊢ (⨅ i, f i).index ≤ ∏ i, (f i).index

Tactic:
by simp_rw [← relIndex_top_right, relIndex_iInf_le]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n : ℕ
h : m ∣ n + 1
⊢ cast 1 = 1

Tactic:
change ((1 % (n + 1) : ℕ) : R) = 1

Goal state after:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n : ℕ
h : m ∣ n + 1
⊢ ↑(1 % (n + 1)) = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ ↑1 = 1

pp: case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ 1 < n✝ + 1 + 1

Tactic:
· exact Nat.cast_one

Goal state after:
case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ 1 < n✝ + 1 + 1
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
exact eq_tsub_of_add_eq rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ (Even n → 0 < x + 1) ∨ 0 = x + 1 ∧ Even n ↔ Even n → 0 < x + 1 ∨ 0 = x + 1

Tactic:
or_comm,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ 0 = x + 1 ∧ Even n ∨ (Even n → 0 < x + 1) ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
x✝ : 0 < n + 4
⊢ (n + 4) * (n + 4).centralBinom ≤ 2 * (n + 4) * (n + 4).centralBinom

Tactic:
by
        rw [mul_assoc]; refine Nat.le_mul_of_pos_left _ zero_lt_two

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

Goal state before:
pp: m n : ℕ
nzm : NeZero m
a : ZMod m
h : a.val < n
⊢ a.cast.val = a.val

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero (NeZero.ne m)
  obtain ⟨n, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero <| by rintro (rfl : n = 0); simp at h
  exact Fin.val_cast_of_lt h

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

Goal state before:
pp: n : ℕ
x y : ℤ
he : ↑x = ↑y
hl : x.natAbs ≤ n / 2
⊢ x.natAbs ≤ y.natAbs

Tactic:
intCast_eq_intCast_iff_dvd_sub

Goal state after:
n : ℕ
x y : ℤ
he : ↑n ∣ y - x
hl : x.natAbs ≤ n / 2
⊢ x.natAbs ≤ y.natAbs
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x y : ℤ
he : ↑x = ↑y
hl : x.natAbs ≤ n / 2
⊢ x.natAbs ≤ y.natAbs

Tactic:
by
  rw [intCast_eq_intCast_iff_dvd_sub] at he
  obtain ⟨m, he⟩ := he
  rw [sub_eq_iff_eq_add] at he
  subst he
  obtain rfl | hm := eq_or_ne m 0
  · rw [mul_zero, zero_add]
  apply hl.trans
  rw [← add_le_add_iff_right x.natAbs]
  refine le_trans (le_trans ((add_le_add_iff_left _).2 hl) ?_) (Int.natAbs_sub_le _ _)
  rw [add_sub_cancel_right, Int.natAbs_mul, Int.natAbs_natCast]
  refine le_trans ?_ (Nat.le_mul_of_pos_right _ <| Int.natAbs_pos.2 hm)
  rw [← mul_two]; apply Nat.div_mul_le_self

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

Goal state before:
pp: b : ℕ
l : List ℕ
⊢ ofDigits b (l ++ [0]) = ofDigits b l

Tactic:
ofDigits_append,

Goal state after:
b : ℕ
l : List ℕ
⊢ ofDigits b l + b ^ l.length * ofDigits b [0] = ofDigits b l
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p n : ℕ
hn : n ≠ 0
⊢ padicValNat p n < n

Tactic:
match p with
  | 0 | 1 => simp [Nat.pos_of_ne_zero hn]
  | p + 2 =>
    apply (p + 2 |>.pow_lt_pow_iff_right <| by lia).mp
    apply Nat.lt_of_le_of_lt ?_ <| Nat.lt_pow_self <| by lia
    exact le_of_dvd (Nat.pos_of_ne_zero hn) pow_padicValNat_dvd

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

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

Tactic:
ofDigits_append,

Goal state after:
b m n : ℕ
⊢ ofDigits b (b.digits n) + b ^ (b.digits n).length * ofDigits b (b.digits m) = n + b ^ (b.digits n).length * m
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
m : ℕ
hm : multiplicity a b < m
⊢ emultiplicity a b < ↑m

Tactic:
rw [hf.emultiplicity_eq_multiplicity]

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
m : ℕ
hm : multiplicity a b < m
⊢ ↑(multiplicity a b) < ↑m
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case inl
p : ℕ
⊢ count p (primeFactorsList 0) = (factorization 0) p

Tactic:
simp [factorization, count]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inr
a : ℕ
b : ℤ
h : b = -↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) (-↑b.natAbs)

Tactic:
emultiplicity_neg,

Goal state after:
case inr
a : ℕ
b : ℤ
h : b = -↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity ↑a ↑b.natAbs
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ (S.prod g).factorization = ∑ x ∈ S, (g x).factorization

Tactic:
classical
    refine Finset.induction_on' S ?_ ?_
    · simp
    · intro x T hxS hTS hxT IH
      have hT : T.prod g ≠ 0 := prod_ne_zero_iff.mpr fun x hx => hS x (hTS hx)
      simp [prod_insert hxT, sum_insert hxT, IH, factorization_mul (hS x hxS) hT]

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

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ p.factorization = single p 1

Tactic:
ext q
  rw [← primeFactorsList_count_eq, primeFactorsList_prime hp, single_apply, count_singleton',
    if_congr eq_comm] <;> rfl

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

Goal state before:
pp: case refine_2
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ (∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L) → L ∈ fixedLengthDigits hb (l + 1)

Tactic:
· rintro ⟨d, hd₁, T, hT, rfl⟩
    exact cons_mem_fixedLengthDigits_succ hb l d hd₁ hT

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_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ IsOfFinOrder x

Tactic:
· rw [isOfFinOrder_iff_pow_eq_one]
    exact Exists.intro n (id ⟨hn, hx⟩)

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case hd
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
⊢ p * orderOf y ∣ orderOf y

Tactic:
← dvd_div_iff_mul_dvd hpy

Goal state after:
case hd
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
⊢ orderOf y ∣ orderOf y / p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Monoid G
x : G
n m : ℕ
hx : IsOfFinOrder x
this : ∀ {n m : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ m = x ^ n ↔ n ≡ m [MOD orderOf x]

Tactic:
ModEq.comm,

Goal state after:
case inr
G : Type u_1
inst✝ : Monoid G
x : G
n m : ℕ
hx : IsOfFinOrder x
this : ∀ {n m : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ m = x ^ n ↔ m ≡ n [MOD orderOf x]
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m n : ℕ
this : ∀ {m n : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ m = x ^ n ↔ n ≡ m [MOD orderOf x]

Tactic:
ModEq.comm,

Goal state after:
case inr
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m n : ℕ
this : ∀ {m n : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ m = x ^ n ↔ m ≡ n [MOD orderOf x]
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n ↦ x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
m : ℕ
hm : 0 < m
hm' : (x ^ n) ^ m = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1

Tactic:
exact ⟨n * m, mul_pos hn hm, by rwa [pow_mul]⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p) =
    x ^ p ^ n + y ^ p ^ n +
      ↑p * x * y * ∑ k ∈ Ioo 0 (p ^ n), x ^ (k - 1) * y ^ (p ^ n - k - 1) * ↑((p ^ n).choose k / p)

Tactic:
mul_assoc _ x,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p) =
    x ^ p ^ n + y ^ p ^ n +
      ↑p * (x * y) * ∑ k ∈ Ioo 0 (p ^ n), x ^ (k - 1) * y ^ (p ^ n - k - 1) * ↑((p ^ n).choose k / p)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n ↦ x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
m : ℕ
hm : 0 < m
hm' : (x ^ n) ^ m = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1

Tactic:
exact ⟨n * m, mul_pos hn hm, by rwa [pow_mul]⟩

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H✝ : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : LeftCancelMonoid G
inst✝² : Finite G
x y : G
n : ℕ
H : Type u_6
inst✝¹ : RightCancelMonoid H
inst✝ : Finite H
this✝ : Finite Hᵐᵒᵖ := Finite.of_equiv H MulOpposite.opEquiv
this : Group Hᵐᵒᵖ := LeftCancelMonoid.groupOfFinite
⊢ Group H

Tactic:
exact (MulEquiv.opOp H).toEquiv.group

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
x : ℕ
⊢ x ∈ {i ∈ Ico 1 n | p ^ i ∣ n} ↔ x ∈ {i ∈ Icc 1 b | p ^ i ∣ n}

Tactic:
simp only [Finset.mem_filter, mem_Ico, mem_Icc, and_congr_left_iff, and_congr_right_iff]

Goal state after:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
x : ℕ
⊢ p ^ x ∣ n → 1 ≤ x → (x < n ↔ x ≤ b)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: 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 : ℕ
⊢ a ^ (n + 1) ∈ S

Tactic:
induction n with
    | zero => rwa [zero_add, pow_one]
    | succ n ih =>
      rw [← hS2, pow_succ]
      exact Set.mul_mem_mul ih ha

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
⊢ derivative (C a * X ^ 2) = C (a * 2) * X

Tactic:
by
  rw [derivative_C_mul_X_pow, Nat.cast_two, pow_one]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
p q : R[X]
h : ¬q.Monic
⊢ q ∣ p %ₘ q - p

Tactic:
simp [modByMonic_eq_of_not_monic, h]

Goal state after:
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
h : p /ₘ (X - C x) = 0
⊢ False

Tactic:
← mul_divByMonic_eq_iff_isRoot.2 hx,

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
this : Decidable (∃ x, p.IsRoot x)
h✝ : ∃ x, p.IsRoot x
x : R
hp : (X - C x) * (p /ₘ (X - C x)) ≠ 0
hx : p.IsRoot x
hpd : 0 < p.degree
h : p /ₘ (X - C x) = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n✝ n : ℕ
ih : Irreducible ((expand R (p ^ n)) f) → Irreducible f
hf : Irreducible ((expand R (p ^ n.succ)) f)
⊢ Irreducible ((expand R p) ((expand R (p ^ n)) f))

Tactic:
rw [pow_succ'] at hf

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n✝ n : ℕ
ih : Irreducible ((expand R (p ^ n)) f) → Irreducible f
hf : Irreducible ((expand R (p * p ^ n)) f)
⊢ Irreducible ((expand R p) ((expand R (p ^ n)) f))
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inl
R : Type u
inst✝ : Ring R
r a : R
h✝ : Subsingleton R
⊢ rootMultiplicity a (C r) = 0

Tactic:
Subsingleton.elim (C r) 0,

Goal state after:
case inl
R : Type u
inst✝ : Ring R
r a : R
h✝ : Subsingleton R
⊢ rootMultiplicity a 0 = 0
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mp.superset
α : Type u
s : Set (Set α)
U s✝ t✝ : Set α
a✝ : GenerateSets s s✝
hVW : s✝ ⊆ t✝
hV : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s✝
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ t✝

Tactic:
rcases hV with ⟨t, hts, ht, htV⟩
      exact ⟨t, hts, ht, htV.trans hVW⟩

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : I.pi t ⊆ eval i ⁻¹' s
⊢ s ∈ f i

Tactic:
rw [← image_subset_iff] at hI

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval i '' I.pi t ⊆ s
⊢ s ∈ f i
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
la : Filter α
lb : Filter β
lc : Filter γ
h₁ : ∀ s ∈ la, Tendsto f (𝓟 sᶜ ×ˢ lb) lc
h₂ : Tendsto f (la ×ˢ ⊤) lc
⊢ Tendsto f (la.coprod lb) lc

Tactic:
simp_all [tendsto_prod_iff, coprod_eq_prod_top_sup_top_prod]
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
la : Filter α
lb : Filter β
lc : Filter γ
h₁ : ∀ s ∈ lb, Tendsto f (la ×ˢ 𝓟 sᶜ) lc
h₂ : Tendsto f (⊤ ×ˢ lb) lc
⊢ Tendsto f (la.coprod lb) lc

Tactic:
simp_all [tendsto_prod_iff, coprod_eq_prod_top_sup_top_prod]
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
⊢ TendstoCofinite (mapDomain f)

Tactic:
classical
  refine (tendstoCofinite_iff_finite_preimage_singleton _).mpr fun x ↦ ?_
  let s := Finset.sup x.support (fun t ↦ (TendstoCofinite.finite_preimage_singleton f t).toFinset)
  let e : s ↪ α := Function.Embedding.subtype (fun u ↦ u ∈ s)
  refine Set.Finite.subset (Set.Finite.image (embDomain e) <| finite_of_degree_le (degree x)) ?_
  simp only [Set.subset_def, Set.mem_preimage, Set.mem_singleton_iff, Set.mem_image,
    Set.mem_ofPred_eq]
  refine fun y hy ↦ ⟨y.comapDomain e e.injective.injOn, ?_, embDomain_comapDomain ?_⟩
  · rw [← hy, degree_mapDomain]
    exact degree_comapDomain_le_of_canonicallyOrderedAdd ..
  · suffices y.support ⊆ s by simpa [e]
    simpa [← hy, mapDomain, sum, Finset.subset_iff, single_apply, s] using
      fun i hi ↦ ⟨i, by simp [hi]⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ ∀ p ∈ normalizedFactors a, ∀ q ∈ normalizedFactors a, p ∣ q → p = q

Tactic:
intro p hp q hq hdvd
  convert!
    normalize_eq_normalize hdvd
      ((prime_of_normalized_factor _ hp).irreducible.dvd_symm
        (prime_of_normalized_factor _ hq).irreducible hdvd) <;>
    apply (normalize_normalized_factor _ ‹_›).symm

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map normalize (normalizedFactors (x * y)) =
    Multiset.map normalize (normalizedFactors x) + Multiset.map normalize (normalizedFactors y)

Tactic:
← Multiset.map_add,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map normalize (normalizedFactors (x * y)) =
    Multiset.map normalize (normalizedFactors x + normalizedFactors y)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case hg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ ∀ x_1 ∈ normalizedFactors (x * y), Irreducible x_1

pp: case h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ (normalizedFactors x + normalizedFactors y).prod ~ᵤ (normalizedFactors (x * y)).prod

Tactic:
· exact irreducible_of_normalized_factor

Goal state after:
case h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ (normalizedFactors x + normalizedFactors y).prod ~ᵤ (normalizedFactors (x * y)).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b c : α
ha : a ∈ normalizedFactors c
hb : b ∈ normalizedFactors c
h : a ~ᵤ b
⊢ normalize a = b

Tactic:
← normalize_normalized_factor b hb,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b c : α
ha : a ∈ normalizedFactors c
hb : b ∈ normalizedFactors c
h : a ~ᵤ b
⊢ normalize a = normalize b
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case succ
α : Type u_5
s : Set α
n : ℕ
ih : n • (fun x ↦ single x 1) '' s = {x | degree x = n ∧ ↑x.support ⊆ s}
⊢ (n + 1) • (fun x ↦ single x 1) '' s = {x | degree x = n + 1 ∧ ↑x.support ⊆ s}

Tactic:
rw [succ_nsmul, ih]
    refine subset_antisymm ?_ fun f ⟨f_deg, f_supp⟩ ↦ ?_
    · simp [Set.subset_def, Set.mem_add, @forall_comm (α →₀ ℕ)]; grind
    obtain ⟨i, hi⟩ : f.support.Nonempty := by aesop
    obtain ⟨x, hx⟩ := le_iff_exists_add'.mp
      (show single i 1 ≤ f by simpa [Nat.one_le_iff_ne_zero] using hi)
    exact ⟨x, by aesop (add simp Set.subset_def), _, ⟨_, f_supp (by simp_all), rfl⟩, hx.symm⟩

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
⊢ nthRootsFinset 0 a = ∅

Tactic:
classical simp [nthRootsFinset_def]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content

Tactic:
rw [← leadingCoeff_eq_zero, leadingCoeff, ← Ne, ← mem_support_iff] at h

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case h.left
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝¹ a : R
a_unit : IsUnit a
a✝ : a ≠ 0
b : R
⊢ IsRelPrime a b

Tactic:
intro p p_dvd_a _

Goal state after:
case h.left
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝² a : R
a_unit : IsUnit a
a✝¹ : a ≠ 0
b p : R
p_dvd_a : p ∣ a
a✝ : p ∣ b
⊢ IsUnit p
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p.IsPrimitive
⊢ C p.content * p.primPart = p

Tactic:
← p.eq_C_content_mul_primPart

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p.IsPrimitive
⊢ p = p