mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case pos.snd
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
a : ↥s
hx : (algebraMap R A) r = -↑a
hr : r = 0
⊢ ↑(Unitization.inl r).toProd.2 = ↑(-↑a).toProd.2

Tactic:
simpa [hr] using hx

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝³ : Ring R
S : Type v
inst✝² : Ring S
J : Ideal R
I : Ideal S
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
⊢ Injective ⇑(quotientMap I f H)

Tactic:
refine (injective_iff_map_eq_zero (quotientMap I f H)).2 fun a ha => ?_
  obtain ⟨r, rfl⟩ := Quotient.mk_surjective a
  rw [quotientMap_mk, Quotient.eq_zero_iff_mem] at ha
  exact Quotient.eq_zero_iff_mem.mpr (h ha)

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : Semiring B
inst✝⁶ : StarRing B
inst✝⁵ : Algebra R B
inst✝⁴ : StarModule R B
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
S : StarSubalgebra R C
g : B →⋆ₐ[R] C
f : A →⋆ₐ[R] B
⊢ ↑(comap f (comap g S)) = ↑(comap (g.comp f) S)

Tactic:
exact Set.preimage_preimage

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

Goal state before:
pp: α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
⊢ m ^ (period m a + n) • a = m ^ n • a

Tactic:
rw [← pow_mod_period_smul, Nat.add_mod_left, pow_mod_period_smul]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l ≠ []
hn : l.Nodup
⊢ l.next (l.getLast h) ⋯ = l.head h

Tactic:
by
  have h1 : l.length - 1 + 1 = l.length := by grind [length_pos_iff]
  simp [getLast_eq_getElem h, head_eq_getElem h, next_getElem l hn (l.length - 1) (by grind), h1]

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

Goal state before:
pp: case mp
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
⊢ (orbit M a).Subsingleton → ∀ (m : M), m • a = a

Tactic:
exact fun h m ↦ h (mem_orbit a m) (mem_orbit_self a)

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

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

Tactic:
apply not_prime_one

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

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

pp: case succ
n : ℕ
n0 : n ≠ 0
a : ℕ
⊢ addOrderOf ↑(a + 1) = n / n.gcd (a + 1)

Tactic:
· simp only [Nat.cast_zero, addOrderOf_zero, Nat.gcd_zero_right,
      Nat.pos_of_ne_zero n0, Nat.div_self]

Goal state after:
case succ
n : ℕ
n0 : n ≠ 0
a : ℕ
⊢ addOrderOf ↑(a + 1) = n / n.gcd (a + 1)
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
⊢ (comap L.subtype (map L.subtype (comap L.subtype J))).relIndex (comap L.subtype K) ≠ 0

Tactic:
comap_map_eq_self_of_injective (subtype_injective L)

Goal state after:
G : Type u_1
inst✝ : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (comap L.subtype J).relIndex (comap L.subtype K) ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case pos
n : ℕ
a b : Fin (n + 1)
h : n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b - (n + 1)) = cast a + cast b - ↑(n + 1)

pp: case neg
n : ℕ
a b : Fin (n + 1)
h : ¬n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b) = cast a + cast b

Tactic:
· rw [Nat.cast_sub h]
    congr

Goal state after:
case neg
n : ℕ
a b : Fin (n + 1)
h : ¬n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b) = cast a + cast b
Module: Mathlib.GroupTheory.Index

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

Tactic:
by
  simp [index_eq_zero_iff_infinite]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ ∀ (a a' : ℕ) (b : ℕ × ℕ),
    (have y := n / a;
        if a * y = n then some (a, y) else none) =
        some b →
      (have y := n / a';
          if a' * y = n then some (a', y) else none) =
          some b →
        a = a'

Tactic:
by simp_all

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
⊢ 0 < ∑ i ∈ range n, x ^ i ↔ Odd n ∨ 0 < x + 1

Tactic:
by
  refine ⟨fun h => ?_, ?_⟩
  · rw [or_iff_not_imp_left, ← not_le, Nat.not_odd_iff_even]
    refine fun hn hx => h.not_ge ?_
    simpa [if_pos hn] using geom_sum_alternating_of_le_neg_one hx n
  · rintro (hn | hx')
    · exact hn.geom_sum_pos
    · exact geom_sum_pos' hx' hn

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ map (Equiv.prodComm ℤ ℤ).toEmbedding z.divisorsAntidiag = z.divisorsAntidiag

Tactic:
by
  ext; simp [mem_divisorsAntidiag]

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

Goal state before:
pp: case inr
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
ha : a ≠ 0
⊢ a.val ^ m < n

Tactic:
· exact lt_of_le_of_lt
         (Nat.pow_le_pow_right (by rwa [gt_iff_lt, ZMod.val_pos]) (Nat.le_succ m)) h

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

Goal state before:
pp: case inr.inr
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ p.maxPowDvdDiv n = (k, l)

Tactic:
rw [← pow_padicValNat_mul_divMaxPow p n, hk, padicValNat, Nat.mul_left_cancel_iff] at h

Goal state after:
case inr.inr
p n k l : ℕ
hn : n ≠ 0
h : l = n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ p.maxPowDvdDiv n = (k, l)

case inr.inr.p
p n k l : ℕ
hn : n ≠ 0
h : p ^ (p.maxPowDvdDiv n).fst * l = p ^ (p.maxPowDvdDiv n).fst * n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ 0 < p ^ (p.maxPowDvdDiv n).fst
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
a : G
inst✝ : IsMulTorsionFree G
ha : a ≠ 1
⊢ ¬∃ n, 0 < n ∧ a ^ n = 1

Tactic:
rintro ⟨n, hn, han⟩

Goal state after:
G : Type u_1
inst✝¹ : Monoid G
a : G
inst✝ : IsMulTorsionFree G
ha : a ≠ 1
n : ℕ
hn : 0 < n
han : a ^ n = 1
⊢ False
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
x✝³ : List ℕ
x✝² : x✝³ ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
x✝¹ : List ℕ
x✝ : x✝¹ ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
h : ofDigits b x✝³ = ofDigits b x✝¹
⊢ x✝³.length = x✝¹.length

Tactic:
by simp_all

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
x✝³ : List ℕ
x✝² : x✝³ ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
x✝¹ : List ℕ
x✝ : x✝¹ ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
h : ofDigits b x✝³ = ofDigits b x✝¹
⊢ ∀ l ∈ x✝³, l < b

Tactic:
by simp_all

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
x✝³ : List ℕ
x✝² : x✝³ ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
x✝¹ : List ℕ
x✝ : x✝¹ ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
h : ofDigits b x✝³ = ofDigits b x✝¹
⊢ ∀ l ∈ x✝¹, l < b

Tactic:
by simp_all

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

Goal state before:
pp: case pos
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : l = 0
⊢ ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2

pp: case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
· simp [hl, fixedLengthDigits_one, Finset.sum_range_id, choose_two_right]

Goal state after:
case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n a : ℕ
hx : x ^ n = 1
c : ℕ
h : a ≡ a + c [MOD n]
hle : a ≤ a + c
⊢ n ∣ c

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n b : ℕ
hx : x ^ n = 1
c : ℕ
h : b + c ≡ b [MOD n]
hle : b ≤ b + c
⊢ n ∣ c

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n m✝ : ℕ
hx : IsOfFinOrder x
m k : ℕ
hmn : m ≤ m + k
⊢ x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]

Tactic:
rw [pow_add, (hx.isUnit.pow _).mul_eq_left, pow_eq_one_iff_modEq]

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n m✝ : ℕ
hx : IsOfFinOrder x
m k : ℕ
hmn : m ≤ m + k
⊢ k ≡ 0 [MOD orderOf x] ↔ m + k ≡ m [MOD orderOf x]
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
h : m + k ≡ m [MOD orderOf x]
⊢ m + k ≡ m + 0 [MOD orderOf x]

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
hx : IsOfFinOrder x
x✝ : y ∈ powers x
n : ℕ
hn : (fun x_1 ↦ x ^ x_1) n = y
⊢ (fun x_1 ↦ x ^ x_1) ↑n = y

Tactic:
by simp_all

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
a✝ : G
⊢ (a✝ ∈ n.divisors.biUnion fun m ↦ {x | orderOf x = m}) ↔ a✝ ∈ {x | x ^ n = 1}

Tactic:
simp [hn, orderOf_dvd_iff_pow_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
n : ℤ
⊢ a ^ n = a ^ (n % ↑(card G))

Tactic:
← zpow_mod_orderOf,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
n : ℤ
⊢ a ^ (n % ↑(orderOf a)) = a ^ (n % ↑(card G))
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ n = a ^ (n % ↑(Nat.card G))

Tactic:
← zpow_mod_orderOf,

Goal state after:
G : Type u_6
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ (n % ↑(orderOf a)) = a ^ (n % ↑(Nat.card G))
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case refine_2
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ Prime ↑p2

Tactic:
exact Nat.prime_of_mem_primeFactors p2.2

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
⊢ g • a = a

Tactic:
have key := smul_mono_right g (pow_smul_le h (Nat.card G - 1))

Goal state after:
G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
key : g • g ^ (Nat.card G - 1) • a ≤ g • a
⊢ g • a = a
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hpn : p ∣ n
hn : n / p ≤ f.natDegree
⊢ n ≤ f.natDegree * p

Tactic:
← Nat.div_mul_cancel hpn

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hpn : p ∣ n
hn : n / p ≤ f.natDegree
⊢ n / p * p ≤ f.natDegree * p
Module: Mathlib.Algebra.Polynomial.Eval.SMul

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ eval₂ g x (s • p) = g s * eval₂ g x p

Tactic:
eval₂_eq_sum,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ((s • p).sum fun e a ↦ g a * x ^ e) = g s * eval₂ g x p
Module: Mathlib.Algebra.Polynomial.Eval.SMul

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ((s • p).sum fun e a ↦ g a * x ^ e) = g s * eval₂ g x p

Tactic:
eval₂_eq_sum,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ((s • p).sum fun e a ↦ g a * x ^ e) = g s * p.sum fun e a ↦ g a * x ^ e
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
⊢ map f x ∣ map f y ↔ y %ₘ x = 0

Tactic:
← modByMonic_eq_zero_iff_dvd (hx.map f),

Goal state after:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
⊢ map f y %ₘ map f x = 0 ↔ y %ₘ x = 0
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: α : Type u_1
s : Set (Set α)
⊢ (∀ {i : Set (Set α)}, i.Finite ∧ i ⊆ s → (⋂₀ i).Nonempty) ↔ ∀ t ⊆ s, t.Finite → (⋂₀ t).Nonempty

Tactic:
by simp only [← and_imp, and_comm]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
x : R
h : p.IsRoot x
⊢ x ∣ p.coeff 0

Tactic:
simpa [h.eq_zero, coeff_zero_eq_eval_zero] using sub_dvd_eval_sub 0 x p

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

Goal state before:
pp: case pos
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Tactic:
rcases subsingleton_or_nontrivial R with hR | hR
    · simp only [eq_iff_true_of_subsingleton]
    · exact
      (div_modByMonic_unique (p₁ /ₘ q + p₂ /ₘ q) _ hq
          ⟨by
            rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div, ← add_assoc,
              add_comm (q * _), modByMonic_add_div],
            (degree_add_le _ _).trans_lt
              (max_lt (degree_modByMonic_lt _ hq) (degree_modByMonic_lt _ hq))⟩).2

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

Goal state before:
pp: case neg
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
⊢ q ∣ p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q)

Tactic:
have : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = (p₁ %ₘ q) * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q) := by ring

Goal state after:
case neg
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
this : (g.comp (X + C t)).coeff 0 = eval t g
⊢ eval t g = (((X - C t) ^ m).comp (X + C t) * g.comp (X + C t)).trailingCoeff

Tactic:
pow_comp,

Goal state after:
case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
this : (g.comp (X + C t)).coeff 0 = eval t g
⊢ eval t g = ((X - C t).comp (X + C t) ^ m * g.comp (X + C t)).trailingCoeff
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
⊢ ∀ a ∈ range (min m n).succ,
    a ∉ range n.succ → (n.choose a * m.descFactorial a) • ((⇑derivative)^[n - a] p * X ^ (m - a)) = 0

Tactic:
by simp_all

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

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
κ : Type u_3
p : κ → Prop
s : (i : ι) → κ → Set (α i)
h : ∀ (i : ι), (f i).HasBasis p (s i)
h_dir : ∀ (I : Set ι) (k : ι → κ), I.Finite → (∀ i ∈ I, p (k i)) → ∃ k₀, p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)
I : Set ι
k : ι → κ
hI : (I, k).1.Finite
hk : ∀ i ∈ (I, k).1, p ((I, k).2 i)
⊢ ∃ i', (i'.1.Finite ∧ p i'.2) ∧ (i'.1.pi fun i ↦ s i i'.2) ⊆ (I, k).1.pi fun i ↦ s i ((I, k).2 i)

Tactic:
rcases h_dir I k hI hk with ⟨k₀, hk₀, hk₀'⟩

Goal state after:
case refine_1
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
κ : Type u_3
p : κ → Prop
s : (i : ι) → κ → Set (α i)
h : ∀ (i : ι), (f i).HasBasis p (s i)
h_dir : ∀ (I : Set ι) (k : ι → κ), I.Finite → (∀ i ∈ I, p (k i)) → ∃ k₀, p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)
I : Set ι
k : ι → κ
hI : (I, k).1.Finite
hk : ∀ i ∈ (I, k).1, p ((I, k).2 i)
k₀ : κ
hk₀ : p k₀
hk₀' : ∀ i ∈ I, s i k₀ ⊆ s i (k i)
⊢ ∃ i', (i'.1.Finite ∧ p i'.2) ∧ (i'.1.pi fun i ↦ s i i'.2) ⊆ (I, k).1.pi fun i ↦ s i ((I, k).2 i)
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: M₀ : Type u_3
inst✝ : CommMonoidWithZero M₀
p : M₀
hp : Prime p
s✝ : Multiset M₀
a : M₀
s : Multiset M₀
ih : p ∣ s.prod → ∃ a ∈ s, p ∣ a
h : p ∣ (a ::ₘ s).prod
⊢ p ∣ a * s.prod

Tactic:
by simpa using h

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

Goal state before:
pp: M₀ : Type u_3
inst✝ : CommMonoidWithZero M₀
s✝ : Multiset (Associates M₀)
p : Associates M₀
hp : Prime p
a : Associates M₀
s : Multiset (Associates M₀)
ih : p ≤ s.prod → ∃ a ∈ s, p ≤ a
h : p ≤ (a ::ₘ s).prod
⊢ p ≤ a * s.prod

Tactic:
by simpa using h

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
hp0 : 0 < p.degree
h : p = 0
⊢ False

Tactic:
by simp_all

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

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

Tactic:
obtain ⟨q, hq⟩ := Multiset.exists_mem_of_ne_zero hs0

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
x✝ : p ∣ a
b : α
hb : a = p * b
hb0 : b = 0
⊢ False

Tactic:
by simp_all

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
⊢ (X - C r).roots = {r}

Tactic:
by
  classical
  ext s
  rw [count_roots, rootMultiplicity_X_sub_C, count_singleton]

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

Goal state before:
pp: σ : Type u_5
s t : Set ℕ
n : ℕ
hn : n ∈ t
g : σ →₀ ℕ
hm : degree g ∈ s
f : σ →₀ ℕ
hgf : g ≤ g + f
e : degree g + n = degree (g + f)
⊢ f ∈ ⇑degree ⁻¹' t

Tactic:
by simp_all

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x = 0
⊢ False

Tactic:
by simp_all

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

Goal state before:
pp: case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ 0 ∉ Multiset.map (fun a ↦ X - C a) s

Tactic:
rw [Multiset.mem_map]

Goal state after:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ ¬∃ a ∈ s, X - C a = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
x✝ : p ∣ a
b : α
hb : a = p * b
hb0 : b = 0
⊢ False

Tactic:
by simp_all

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

Goal state before:
pp: α : Type u_5
s : Set α
n : ℕ
ih : n • (fun x ↦ single x 1) '' s = {x | degree x = n ∧ ↑x.support ⊆ s}
f : α →₀ ℕ
x✝ : f ∈ {x | degree x = n + 1 ∧ ↑x.support ⊆ s}
f_deg : degree f = n + 1
f_supp : ↑f.support ⊆ s
i : α
hi : i ∈ f.support
x : α →₀ ℕ
hx : f = x + single i 1
⊢ i ∈ ↑f.support

Tactic:
by simp_all

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
⊢ p.count 0 = 0

Tactic:
by
  simp only [count, dif_pos hp, bcount, Multiset.count_zero]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
⊢ ∃ a_1, ∃ (h : a_1 ∈ UniqueFactorizationMonoid.factors a), ⟨Associates.mk a_1, ⋯⟩ = ⟨Associates.mk p, ⋯⟩

Tactic:
use q

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
⊢ ∃ (h : q ∈ UniqueFactorizationMonoid.factors a), ⟨Associates.mk q, ⋯⟩ = ⟨Associates.mk p, ⋯⟩