mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
a✝¹ : α
l✝ : List α
a✝ : Chain r₁ ↑l✝ → Chain r₂ ↑l✝
p : Chain r₁ ↑(a✝¹ :: l✝)
⊢ Chain r₂ ↑(a✝¹ :: l✝)

Tactic:
rw [chain_coe_cons] at p ⊢
    exact p.imp H

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

Goal state before:
pp: case inr
n k : ℕ
hn : n ≠ 0
⊢ (n ^ (k + 1)).primeFactors = n.primeFactors

Tactic:
induction k with
  | zero => simp
  | succ k ih => rw [pow_succ', primeFactors_mul hn (pow_ne_zero _ hn), ih, Finset.union_idempotent]

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

Goal state before:
pp: p a b : ℕ
hpb : p ∈ b.primeFactorsList
ha : a ≠ 0
⊢ p ∈ (a * b).primeFactorsList

Tactic:
by
  rw [mul_comm]
  exact mem_primeFactorsList_mul_left hpb ha

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case pos
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : n = 0
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f

pp: case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f

Tactic:
· simp [hn]

Goal state after:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
α : Type u_1
inst✝ : Semiring α
b : α
d : ℕ
L : List ℕ
ih : ofDigits b L = List.foldr (fun x y ↦ ↑x + b * y) 0 L
⊢ ofDigits b (d :: L) = List.foldr (fun x y ↦ ↑x + b * y) 0 (d :: L)

Tactic:
dsimp [ofDigits]; rw [ih]

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

Goal state before:
pp: p i n : ℕ
h : 2 ≤ p
⊢ n / p ^ i = ofDigits p (List.drop i (p.digits n))

Tactic:
by
  convert!
    ofDigits_div_pow_eq_ofDigits_drop i (zero_lt_of_lt h) (p.digits n)
      (fun l hl ↦ digits_lt_base h hl)
  exact (ofDigits_digits p n).symm

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

Goal state before:
pp: a b m n✝ p n : ℕ
⊢ ∀ (a : ℕ), a ∈ n.primeFactors ↔ (if Prime a then padicValNat a n else 0) ≠ 0

Tactic:
simp [not_or]

Goal state after:
a b m n✝ p n : ℕ
⊢ ∀ (a : ℕ), Prime a → (a ∣ n ∧ ¬n = 0 ↔ ¬a = 1 ∧ ¬n = 0 ∧ a ∣ n)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a : α
hp : Prime p
hfin : FiniteMultiplicity p a
k✝ k : ℕ
ha : FiniteMultiplicity p a
⊢ FiniteMultiplicity p (a ^ (k + 1))

Tactic:
_root_.pow_succ'

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a : α
hp : Prime p
hfin : FiniteMultiplicity p a
k✝ k : ℕ
ha : FiniteMultiplicity p a
⊢ FiniteMultiplicity p (a * a ^ k)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b

Tactic:
by
  by_cases hfin : FiniteMultiplicity p (a * b)
  · rw [hfin.emultiplicity_eq_multiplicity, hfin.mul_left.emultiplicity_eq_multiplicity,
      hfin.mul_right.emultiplicity_eq_multiplicity]
    norm_cast
    exact multiplicity_mul hp hfin
  · rw [emultiplicity_eq_top.mpr hfin, eq_comm, ENat.add_eq_top, emultiplicity_eq_top,
      emultiplicity_eq_top]
    simpa only [FiniteMultiplicity.mul_iff hp, not_and_or] using hfin

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

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

Tactic:
contrapose hr0
    exact (add_eq_zero.1 hr0).2

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case succ
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a : α
hp : Prime p
k : ℕ
hk : emultiplicity p (a ^ k) = ↑k * emultiplicity p a
⊢ emultiplicity p (a ^ (k + 1)) = ↑(k + 1) * emultiplicity p a

Tactic:
simp [pow_succ, emultiplicity_mul hp, hk, add_mul]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
x : G
H : Type u_6
inst✝ : Monoid H
y : H
⊢ orderOf x = orderOf y ↔ ∀ (n : ℕ), IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ↔ IsPeriodicPt (fun x ↦ y * x) n 1

Tactic:
← minimalPeriod_eq_minimalPeriod_iff,

Goal state after:
G : Type u_1
inst✝¹ : Monoid G
x : G
H : Type u_6
inst✝ : Monoid H
y : H
⊢ orderOf x = orderOf y ↔ minimalPeriod (fun x_1 ↦ x * x_1) 1 = minimalPeriod (fun x ↦ y * x) 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
hx : IsOfFinOrder x
x✝ : y ∈ zpowers x
i : ℤ
hi : (fun x_1 ↦ x ^ x_1) i = y
⊢ x ^ ↑(i % ↑(orderOf x)).natAbs = y

Tactic:
Int.natAbs_of_nonneg <| Int.emod_nonneg _ <|
      Int.natCast_ne_zero_iff_pos.2 <| hx.orderOf_pos,

Goal state after:
G : Type u_1
inst✝ : Group G
x y : G
hx : IsOfFinOrder x
x✝ : y ∈ zpowers x
i : ℤ
hi : (fun x_1 ↦ x ^ x_1) i = y
⊢ x ^ (i % ↑(orderOf x)) = y
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ↑n ≤ emultiplicity p ((p ^ n).choose k) + emultiplicity p k

Tactic:
by rw [← hp.emultiplicity_pow_self]; exact emultiplicity_le_emultiplicity_choose_add hp _ _

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

Goal state before:
pp: case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ emultiplicity 2 (bit true n)! < ↑(bit true n)

Tactic:
suffices emultiplicity 2 (2 * n + 1) + emultiplicity 2 (2 * n)! < ↑(2 * n) + 1 by
        simpa [emultiplicity_mul, h2, prime_two, bit, factorial]

Goal state after:
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ emultiplicity 2 (2 * n + 1) + emultiplicity 2 (2 * n)! < ↑(2 * n) + 1
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.divX.natDegree = p.natDegree - 1

Tactic:
by
  apply map_natDegree_eq_sub (φ := divX_hom)
  · intro f
    simpa [divX_hom, divX_eq_zero_iff] using eq_C_of_natDegree_eq_zero
  · intro n c c0
    rw [← C_mul_X_pow_eq_monomial, divX_hom_toFun, divX_C_mul, divX_X_pow]
    split_ifs with n0
    · simp [n0]
    · exact natDegree_C_mul_X_pow (n - 1) c c0

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

Goal state before:
pp: a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
ha : a = c ^ n
⊢ a = c ^ n ∧ b = c ^ m

Tactic:
refine ⟨ha, ?_⟩

Goal state after:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
ha : a = c ^ n
⊢ b = c ^ m
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
x : G
h✝ : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : |x| ^ n = 1
h : 1 < |x|
⊢ False

Tactic:
· exact ((one_lt_pow₀ h hn.ne').ne' hx).elim

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : o = m * n
⊢ (p ^ m).coeff o = a ^ m

Tactic:
subst h h_pow_bas
    exact coeff_pow_of_natDegree_le ‹_›

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
x✝ : X ∣ f
g : R[X]
hfg : f = X * g
⊢ f.coeff 0 = 0

Tactic:
by rw [hfg, coeff_X_mul_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
⊢ (p %ₘ q).natDegree < q.natDegree

Tactic:
by
  by_cases hpq : p %ₘ q = 0
  · rw [hpq, natDegree_zero, Nat.pos_iff_ne_zero]
    contrapose hq
    exact eq_one_of_monic_natDegree_zero hmq hq
  · have := Nontrivial.of_polynomial_ne hpq
    exact natDegree_lt_natDegree hpq (degree_modByMonic_lt p hmq)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
p : R[X]
⊢ eval₂ (algebraMap A B) x (map (algebraMap R A) p) = eval₂ (algebraMap R B) x p

Tactic:
eval₂_map,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
p : R[X]
⊢ eval₂ ((algebraMap A B).comp (algebraMap R A)) x p = eval₂ (algebraMap R B) x p
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
n : ℕ
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
⊢ n ∈ (derivative p).support ↔ n + 1 ∈ p.support

Tactic:
by
  suffices ¬p.coeff (n + 1) * (n + 1 : ℕ) = 0 ↔ coeff p (n + 1) ≠ 0 by
    simpa only [mem_support_iff, coeff_derivative, Ne, Nat.cast_succ]
  rw [← nsmul_eq_mul', smul_eq_zero]
  simp only [Nat.succ_ne_zero, false_or]

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

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
⊢ (⨅ i, l i).HasBasis (fun If ↦ If.fst.Finite ∧ ∀ (i : ↑If.fst), p (↑i) (If.snd i)) fun If ↦ ⋂ i, s (↑i) (If.snd i)

Tactic:
refine ⟨fun t => ⟨fun ht => ?_, ?_⟩⟩
  · rcases (HasBasis.iInf' hl).mem_iff.mp ht with ⟨⟨I, f⟩, ⟨hI, hf⟩, hsub⟩
    exact ⟨⟨I, fun i => f i⟩, ⟨hI, Subtype.forall.mpr hf⟩, trans (iInter_subtype _ _) hsub⟩
  · rintro ⟨⟨I, f⟩, ⟨hI, hf⟩, hsub⟩
    grw [← hsub]
    cases hI.nonempty_fintype
    exact iInter_mem.2 fun i => mem_iInf_of_mem ↑i <| (hl i).mem_of_mem <| hf _

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

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ U ∈ generate (⋃ i, (s i).sets) → ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Tactic:
mem_generate_iff

Goal state after:
case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ (∃ t ⊆ ⋃ i, (s i).sets, t.Finite ∧ ⋂₀ t ⊆ U) → ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case refine_1
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
⊢ (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) i ∈ s i

pp: case refine_2
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
hi : i ∉ I
⊢ (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) i = univ

pp: case refine_3
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ⋂ i, V i = ⋂ x, (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) ↑x ∧
    ⋂ i, V i = ⋂ i, (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) i

Tactic:
· dsimp only
    split_ifs
    exacts [hV ⟨i,_⟩, univ_mem]

Goal state after:
case refine_2
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
hi : i ∉ I
⊢ (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) i = univ

case refine_3
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ⋂ i, V i = ⋂ x, (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) ↑x ∧
    ⋂ i, V i = ⋂ i, (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) i
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ((a ⊓ ￢a ≤ a ⊔ (a ⊔ b) ∧ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)) ∧ a ⊓ ￢a ≤ a ⊔ b ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b) ∧
    a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b)) ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)

Tactic:
refine ⟨⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩, ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (a ⊔ b)

case refine_2
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)

case refine_3
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ b

case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b

case refine_5
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b))

case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
γ : Type u_3
f : Filter α
g : Filter γ
p : α × γ × γ → Prop
⊢ (∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x) → ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.1, x.2, x.2)

Tactic:
intro h
  obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h
  exact (ht.prod_mk hs.diag_of_prod).mono fun x hx => by simp only [hst hx.1 hx.2]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
⊢ (Pi.map f '' (I, s).1.pi fun i ↦ id ((I, s).2 i)) ∈ pi fun i ↦ map (f i) (l i)

Tactic:
← univ_pi_piecewise_univ,

Goal state after:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
⊢ Pi.map f '' univ.pi ((I, s).1.piecewise (fun i ↦ id ((I, s).2 i)) fun x ↦ univ) ∈ pi fun i ↦ map (f i) (l i)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case e_a
R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
j : ι
hj : j ∈ s
⊢ (f i ::ₘ Multiset.map f (s.erase j)).prod * derivative (f j) =
    (Multiset.map f ((i ::ₘ s).erase j)).prod * derivative (f j)

Tactic:
← Multiset.map_cons

Goal state after:
case e_a
R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
j : ι
hj : j ∈ s
⊢ (Multiset.map f (i ::ₘ s.erase j)).prod * derivative (f j) =
    (Multiset.map f ((i ::ₘ s).erase j)).prod * derivative (f j)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : DecidableEq R
S : Multiset R
r : R
hr : r ∈ S
this :
  ↑(evalRingHom r) (Multiset.map (fun a ↦ X - C a) (S.erase r)).prod =
    (Multiset.map (⇑↑(evalRingHom r)) (Multiset.map (fun a ↦ X - C a) (S.erase r))).prod
⊢ eval r (derivative (Multiset.map (fun a ↦ X - C a) (r ::ₘ S.erase r)).prod) =
    (Multiset.map (fun a ↦ r - a) (S.erase r)).prod

Tactic:
simpa using this

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun t ↦ ⋯.toFinset
e : ↥s ↪ α := Function.Embedding.subtype fun u ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
⊢ degree (comapDomain (⇑e) y ⋯) ≤ degree y

Tactic:
exact degree_comapDomain_le_of_canonicallyOrderedAdd ..

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

Goal state before:
pp: M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : (a : M₀) → DecidablePred (Associated a)
s : Multiset M₀
n : M₀
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1
⊢ s.prod ∣ n

Tactic:
induction s using Multiset.induction_on generalizing n with

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
⊢ (p + -C a).degree = p.degree

Tactic:
← C_neg

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
hp0 : 0 < p.degree
⊢ (p + C (-a)).degree = p.degree
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ p.roots = 0 ↔ p = 0 ∨ p.IsRoot = ⊥

Tactic:
by
  rcases eq_or_ne p 0 with rfl | hp0; · simp
  simp [roots_eq_zero_iff_isRoot_eq_bot hp0, hp0]

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:
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.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Finset R
⊢ ∏ a ∈ s, (X - C a) ≠ 0

Tactic:
· refine prod_ne_zero_iff.mpr (fun a _ => X_sub_C_ne_zero a)

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Finset R
⊢ (∏ a ∈ s, (X - C a)).roots = s.val

Tactic:
apply (roots_prod (fun a => X - C a) s ?_).trans
  · simp_rw [roots_X_sub_C]
    rw [Multiset.bind_singleton, Multiset.map_id']
  · refine prod_ne_zero_iff.mpr (fun a _ => X_sub_C_ne_zero a)

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

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

Tactic:
hxb

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
h✝ : Nontrivial α
⊢ normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum

Tactic:
induction s using Multiset.induction with
  | empty => simp
  | cons _ _ IH =>
    rw [Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons, normalizedFactors_mul, IH]
    · exact fun h ↦ hs (Multiset.mem_cons_of_mem h)
    · exact fun h ↦ hs (h ▸ Multiset.mem_cons_self _ _)
    · apply Multiset.prod_ne_zero
      exact fun h ↦ hs (Multiset.mem_cons_of_mem h)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ (if 1 = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors 1)).prod) = 1

Tactic:
by nontriviality α; simp

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:
mem_rootSet',

Goal state after:
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
⊢ map (algebraMap T S) p ≠ 0 ∧ (aeval a) p = 0 ↔ p ≠ 0 ∧ (aeval a) p = 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case succ
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
n : ℕ
ih : (∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R) → ↑n ! ∈ nonZeroDivisors R
hnzd : ∀ m ≤ n + 1, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ ↑(n + 1)! ∈ nonZeroDivisors R

Tactic:
rw [Nat.factorial_succ, Nat.cast_mul, mul_mem_nonZeroDivisors]

Goal state after:
case succ
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
n : ℕ
ih : (∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R) → ↑n ! ∈ nonZeroDivisors R
hnzd : ∀ m ≤ n + 1, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ ↑(n + 1) ∈ nonZeroDivisors R ∧ ↑n ! ∈ nonZeroDivisors R
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
⊢ p % q = p

Tactic:
by
    have : ¬degree (q * C (leadingCoeff q)⁻¹) ≤ degree p :=
      not_le_of_gt <| by rwa [degree_mul_leadingCoeff_inv q hq0]
    rw [mod_def, modByMonic, dif_pos (monic_mul_leadingCoeff_inv hq0)]
    unfold divModByMonicAux
    dsimp
    simp only [this, false_and, if_false]

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

Goal state before:
pp: case neg
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
a : A
hp0 : ¬p = 0
⊢ rootMultiplicity a p = rootMultiplicity (f a) (map f p)

Tactic:
apply le_antisymm (le_rootMultiplicity_map ((Polynomial.map_ne_zero_iff hf).mpr hp0) a)

Goal state after:
case neg
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
a : A
hp0 : ¬p = 0
⊢ rootMultiplicity (f a) (map f p) ≤ rootMultiplicity a p
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
⊢ Multiset.map (⇑f) p.roots ≤ (map f p).roots

Tactic:
by
  by_cases hp0 : p = 0
  · simp only [hp0, roots_zero, Multiset.map_zero, Polynomial.map_zero, le_rfl]
  exact map_roots_le ((Polynomial.map_ne_zero_iff hf).mpr hp0)

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : Associates α
ha0 : a ≠ 0
a0 : α
hm : p ∈ ↑(factors' a0)
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∈ Multiset.map Subtype.val (factors' a0)

Tactic:
apply Multiset.mem_map.mpr

Goal state after:
case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : Associates α
ha0 : a ≠ 0
a0 : α
hm : p ∈ ↑(factors' a0)
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ ∃ a ∈ factors' a0, ↑a = p
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ ⟨Associates.mk p, ⋯⟩ ∈ factors' a → p ∣ a

pp: case mpr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ p ∣ a → ⟨Associates.mk p, ⋯⟩ ∈ factors' a

Tactic:
· rw [← mk_dvd_mk]
    apply dvd_of_mem_factors'
    apply ha0

Goal state after:
case mpr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ p ∣ a → ⟨Associates.mk p, ⋯⟩ ∈ factors' a
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
hroots : p.roots.card = p.natDegree
⊢ Multiset.map (⇑f) p.roots = (map f p).roots

Tactic:
apply Multiset.eq_of_le_of_card_le (map_roots_le_of_injective p hf)
  simpa only [Multiset.card_map, hroots] using card_roots_map_le_natDegree p

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
⊢ (∀ (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

Tactic:
simp [hp0, natDegree_mul_leadingCoeff_inv]

Goal state after: