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

Goal state before:
pp: z : ℤ
⊢ image Prod.fst z.divisorsAntidiag = z.divisors

Tactic:
ext
  simp [Eq.comm, dvd_def]

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

Goal state before:
pp: m : ℕ
inst✝¹ : NeZero m
n : ℕ
inst✝ : NeZero n
a : ZMod m
⊢ a.cast.val < m

Tactic:
by
  obtain ⟨m, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero (NeZero.ne m)
  by_cases! h : m < n
  · obtain ⟨n, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero (NeZero.ne n)
    rw [← natCast_val, val_cast_of_lt]
    · apply a.val_lt
    apply lt_of_le_of_lt (Nat.le_of_lt_succ (ZMod.val_lt a)) h
  · apply lt_of_lt_of_le (ZMod.val_lt _) (le_trans h (Nat.le_succ m))

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

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

Tactic:
by rw [← mul_assoc]; linarith

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

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

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero <| by rintro (rfl : n = 0); simp at h

Goal state after:
m : ℕ
nzm : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
h : a.val < n + 1
⊢ a.cast.val = a.val
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m k n : ℕ
| (∃ y, m * y + k = n) ↔ ↑n = ↑k ∧ k ≤ n

Tactic:
enter [1, 1, y]

Goal state after:
m k n y : ℕ
| m * y + k = n
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p m : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hp : 1 < p ∧ p * m ≠ 0
⊢ p * m / (p * p) < p * m / p

Tactic:
have hp₀ : 0 < p := Nat.lt_trans Nat.one_pos hp.1

Goal state after:
p m : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hp : 1 < p ∧ p * m ≠ 0
hp₀ : 0 < p
⊢ p * m / (p * p) < p * m / p
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ (n✝ + 1) % (b + 2) + (b + 1 + 1) * ofDigits (b + 1 + 1) ((b + 2).digits ((n✝ + 1) / (b + 2))) = n✝ + 1

Tactic:
h _ (Nat.div_lt_self' _ b)

Goal state after:
case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ (n✝ + 1) % (b + 2) + (b + 1 + 1) * ((n✝ + 1) / (b + 2)) = n✝ + 1
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case case1
p✝ p e q : ℕ
hqp : q % p = 0
hdvd : ¬p * p ∣ (e, q).snd
hp : 1 < p ∧ (e, q).snd * (p * p) ^ (e, q).fst ≠ 0
hmod : (e, q).snd * (p * p) ^ (e, q).fst % p = 0
heq : go ((e, q).snd * (p * p) ^ (e, q).fst) (p * p) ⋯ = (e, q)
⊢ (2 * e + 1, q / p).snd * p ^ (2 * e + 1, q / p).fst = (e, q).snd * (p * p) ^ (e, q).fst ∧ ¬p ∣ (2 * e + 1, q / p).snd

Tactic:
have hp₀ : 0 < p := Nat.lt_trans Nat.one_pos hp.1

Goal state after:
case case1
p✝ p e q : ℕ
hqp : q % p = 0
hdvd : ¬p * p ∣ (e, q).snd
hp : 1 < p ∧ (e, q).snd * (p * p) ^ (e, q).fst ≠ 0
hmod : (e, q).snd * (p * p) ^ (e, q).fst % p = 0
heq : go ((e, q).snd * (p * p) ^ (e, q).fst) (p * p) ⋯ = (e, q)
hp₀ : 0 < p
⊢ (2 * e + 1, q / p).snd * p ^ (2 * e + 1, q / p).fst = (e, q).snd * (p * p) ^ (e, q).fst ∧ ¬p ∣ (2 * e + 1, q / p).snd
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ n ≡ (b'.digits n).sum [MOD b]

Tactic:
rw [← ofDigits_one]

Goal state after:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ n ≡ ofDigits 1 (b'.digits n) [MOD b]
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : 1 ∉ periodicPts fun x_1 ↦ x * x_1
⊢ 0 = n ↔ IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 ↦ x * x_1) m 1

Tactic:
iff_false_left h.ne

Goal state after:
case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : 1 ∉ periodicPts fun x_1 ↦ x * x_1
⊢ ¬(IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 ↦ x * x_1) m 1)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p k n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ p ^ k ∣ n ↔ k ≤ n.factorization p

Tactic:
rw [← factorization_le_iff_dvd (Nat.pow_pos pp.pos).ne' hn, pp.factorization_pow, single_le_iff]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
⊢ (Injective fun n ↦ x ^ n) ↔ ¬IsOfFinOrder x

Tactic:
refine ⟨fun h => not_isOfFinOrder_of_injective_pow h, fun h n m hnm => ?_⟩

Goal state after:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
n m : ℕ
hnm : (fun n ↦ x ^ n) n = (fun n ↦ x ^ n) m
⊢ n = m
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
⊢ (Injective fun n ↦ x ^ n) ↔ ¬IsOfFinOrder x

Tactic:
refine ⟨fun h => not_isOfFinOrder_of_injective_pow h, fun h n m hnm => ?_⟩

Goal state after:
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
h : ¬IsOfFinOrder x
n m : ℕ
hnm : (fun n ↦ x ^ n) n = (fun n ↦ x ^ n) m
⊢ n = m
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
a : G
⊢ of' k G a /ᵒᶠ a = 1

Tactic:
simpa only [one_mul] using mul_of'_divOf (1 : k[G]) a

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ p.divX.coeff n = p.coeff (1 + n)

Tactic:
cases p

Goal state after:
case ofFinsupp
R : Type u
n : ℕ
inst✝ : Semiring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := toFinsupp✝ }.divX.coeff n = { toFinsupp := toFinsupp✝ }.coeff (1 + n)
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
p : R[X]
m : ℕ
h_deg_le : p.degree ≤ ↑m
coeff_ne_zero : p.coeff (WithBot.unbotD 0 ↑m) ≠ 0
hh : ↑m ≠ ⊥
⊢ p.degree = ↑m

Tactic:
exact degree_eq_of_le_of_coeff_ne_zero ‹_› ‹_›

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

Goal state before:
pp: case neg.hnc
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
a✝ : k ∈ f.support
⊢ ¬p * k = n

Tactic:
exact fun hkn => h ⟨k, hkn.symm⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ f.coeff (n * p / p) = f.coeff n

Tactic:
Nat.mul_div_cancel _ hp

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ f.coeff n = f.coeff n
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ ¬q.degree ≤ p.degree → (p %ₘ q).degree < q.degree

Tactic:
unfold modByMonic divModByMonicAux
          dsimp
          rw [dif_pos hq, if_neg h]
          exact lt_of_not_ge

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∑ x ∈ antidiagonal (n * p), f.coeff x.1 * ((expand R p) g).coeff x.2 =
    ∑ x ∈ antidiagonal n, (contract p f).coeff x.1 * g.coeff x.2

Tactic:
← sum_subset
    (s₁ := (antidiagonal n).image fun x ↦ (x.1 * p, x.2 * p)),

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∑ x ∈ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n), f.coeff x.1 * ((expand R p) g).coeff x.2 =
    ∑ x ∈ antidiagonal n, (contract p f).coeff x.1 * g.coeff x.2

case h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) ⊆ antidiagonal (n * p)

case hf
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ x ∈ antidiagonal (n * p),
    x ∉ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) → f.coeff x.1 * ((expand R p) g).coeff x.2 = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg.succ
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
this : coeff 0 n = f.coeff (n + 1) * (↑n + 1)
⊢ 0 = f.coeff (n + 1)

Tactic:
coeff_zero,

Goal state after:
case neg.succ
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
this : 0 = f.coeff (n + 1) * (↑n + 1)
⊢ 0 = f.coeff (n + 1)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
⊢ f /ₘ g = q ∧ f %ₘ g = r

Tactic:
nontriviality R
  have h₁ : r - f %ₘ g = -g * (q - f /ₘ g) :=
    eq_of_sub_eq_zero
      (by
        rw [← sub_eq_zero_of_eq (h.1.trans (modByMonic_add_div f g).symm)]
        simp [mul_add, sub_eq_add_neg, add_comm, add_left_comm, add_assoc])
  have h₂ : degree (r - f %ₘ g) = degree (g * (q - f /ₘ g)) := by simp [h₁]
  have h₄ : degree (r - f %ₘ g) < degree g :=
    calc
      degree (r - f %ₘ g) ≤ max (degree r) (degree (f %ₘ g)) := degree_sub_le _ _
      _ < degree g := max_lt_iff.2 ⟨h.2, degree_modByMonic_lt _ hg⟩
  have h₅ : q - f /ₘ g = 0 :=
    _root_.by_contradiction fun hqf =>
      not_le_of_gt h₄ <|
        calc
          degree g ≤ degree g + degree (q - f /ₘ g) := by
            rw [degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hqf]
            norm_cast
            exact Nat.le_add_right _ _
          _ = degree (r - f %ₘ g) := by rw [h₂, degree_mul']; simpa [Monic.def.1 hg]
  exact ⟨Eq.symm <| eq_of_sub_eq_zero h₅, Eq.symm <| eq_of_sub_eq_zero <| by simpa [h₅] using h₁⟩

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

Goal state before:
pp: case isFalse
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h : ¬p = 0
⊢ Nat.find ⋯ = WithTop.untopD 1 ↑(Nat.find ⋯)

Tactic:
rw [untopD_coe_enat]

Goal state after:
case isFalse
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h : ¬p = 0
⊢ Nat.find ⋯ = Nat.find ⋯
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
this : (p %ₘ (X - C a)).degree < 1
⊢ p %ₘ (X - C a) = C (eval a p)

Tactic:
have : degree (p %ₘ (X - C a)) ≤ 0 := by
    revert this
    cases degree (p %ₘ (X - C a))
    · exact fun _ => bot_le
    · exact fun h => WithBot.coe_le_coe.2 (Nat.le_of_lt_succ (WithBot.coe_lt_coe.1 h))

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
this✝ : (p %ₘ (X - C a)).degree < 1
this : (p %ₘ (X - C a)).degree ≤ 0
⊢ p %ₘ (X - C a) = C (eval a p)
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
coeff_zero,

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

Goal state before:
pp: α : Type u_2
a : α
⊢ (pure a).ker = {a}

Tactic:
rw [← principal_singleton, ker_principal]

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

Goal state before:
pp: α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s

Tactic:
have := ht.to_subtype

Goal state after:
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite ↑t
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
hq : q ≠ 0
hpq : p ∣ q
x : R
⊢ rootMultiplicity x p ≤ rootMultiplicity x q

Tactic:
by
  obtain ⟨_, rfl⟩ := hpq
  exact Nat.le_of_add_right_le <| le_rootMultiplicity_mul x hq

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

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

Tactic:
rw [← rootMultiplicity_le_iff p0]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
h : ∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ s
i : ι
⊢ ∃ t₁ ∈ f i, eval i ⁻¹' t₁ ⊆ (fun k i ↦ m i (k i)) ⁻¹' s

Tactic:
obtain ⟨t, H, hH⟩ := h i

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
h : ∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ s
i : ι
t : Set (β i)
H : m i ⁻¹' t ∈ f i
hH : eval i ⁻¹' t ⊆ s
⊢ ∃ t₁ ∈ f i, eval i ⁻¹' t₁ ⊆ (fun k i ↦ m i (k i)) ⁻¹' s
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
inst✝ : g.NeBot
⊢ map Prod.fst (f ×ˢ g) = f

Tactic:
by
  ext s
  simp only [mem_map, mem_prod_iff_left, mem_preimage, eventually_const, ← subset_def,
    exists_mem_subset_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ comap ((Prod.fst ∘ Prod.fst) ∘ ⇑(Equiv.prodAssoc α β γ).symm) f ⊓
        comap ((Prod.snd ∘ Prod.fst) ∘ ⇑(Equiv.prodAssoc α β γ).symm) g ⊓
      comap (Prod.snd ∘ ⇑(Equiv.prodAssoc α β γ).symm) h =
    comap Prod.fst f ⊓ (comap (Prod.fst ∘ Prod.snd) g ⊓ comap (Prod.snd ∘ Prod.snd) h)

Tactic:
inf_assoc,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ comap ((Prod.fst ∘ Prod.fst) ∘ ⇑(Equiv.prodAssoc α β γ).symm) f ⊓
      (comap ((Prod.snd ∘ Prod.fst) ∘ ⇑(Equiv.prodAssoc α β γ).symm) g ⊓
        comap (Prod.snd ∘ ⇑(Equiv.prodAssoc α β γ).symm) h) =
    comap Prod.fst f ⊓ (comap (Prod.fst ∘ Prod.snd) g ⊓ comap (Prod.snd ∘ Prod.snd) h)
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ comap (Prod.fst ∘ ⇑(Equiv.prodAssoc α β γ)) f ⊓
      (comap ((Prod.fst ∘ Prod.snd) ∘ ⇑(Equiv.prodAssoc α β γ)) g ⊓
        comap ((Prod.snd ∘ Prod.snd) ∘ ⇑(Equiv.prodAssoc α β γ)) h) =
    comap (Prod.fst ∘ Prod.fst) f ⊓ comap (Prod.snd ∘ Prod.fst) g ⊓ comap Prod.snd h

Tactic:
inf_assoc,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ comap (Prod.fst ∘ ⇑(Equiv.prodAssoc α β γ)) f ⊓
      (comap ((Prod.fst ∘ Prod.snd) ∘ ⇑(Equiv.prodAssoc α β γ)) g ⊓
        comap ((Prod.snd ∘ Prod.snd) ∘ ⇑(Equiv.prodAssoc α β γ)) h) =
    comap (Prod.fst ∘ Prod.fst) f ⊓ (comap (Prod.snd ∘ Prod.fst) g ⊓ comap Prod.snd h)
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
B : Filter β
⊢ map (Function.uncurry f) (pure a ×ˢ B) = map (f a) B

Tactic:
by
  rw [Filter.pure_prod]; rfl

Goal state after:
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
⊢ p / GCDMonoid.gcd p q ≠ 0

Tactic:
by
  obtain ⟨r, hr⟩ := GCDMonoid.gcd_dvd_left p q
  obtain ⟨pq0, r0⟩ : GCDMonoid.gcd p q ≠ 0 ∧ r ≠ 0 := mul_ne_zero_iff.mp (hr ▸ hp)
  nth_rw 1 [hr]
  rw [mul_comm, mul_div_cancel_right₀ _ pq0]
  exact r0

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ ∀ {a : Associates α}, Irreducible a ↔ Prime a

Tactic:
by
      rw [← Associates.irreducible_iff_prime_iff]
      apply UniqueFactorizationMonoid.irreducible_iff_prime

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

Goal state before:
pp: case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ roots 1 = 0 • p.roots

Tactic:
roots_one,

Goal state after:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ ∅ = 0 • p.roots
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Finset R
⊢ (s.val.bind fun a ↦ {a}) = s.val

Tactic:
rw [Multiset.bind_singleton, Multiset.map_id']

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

Goal state before:
pp: case a
α : 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 α := ⋯
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ (p ::ₘ fx).prod ~ᵤ (fa + fb).prod

Tactic:
calc
            Multiset.prod (p ::ₘ fx) ~ᵤ a * b := by
              rw [hx, Multiset.prod_cons]; exact hfx.2.mul_left _
            _ ~ᵤ fa.prod * fb.prod := hfa.2.symm.mul_mul hfb.2.symm
            _ = _ := by rw [Multiset.prod_add]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ (s.bind fun a ↦ {a}) = s

Tactic:
rw [Multiset.bind_singleton, Multiset.map_id']

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

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

pp: case inr.cons.hx
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ a✝ ≠ 0

pp: case inr.cons.hy
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ s✝.prod ≠ 0

Tactic:
· exact fun h ↦ hs (Multiset.mem_cons_of_mem h)

Goal state after:
case inr.cons.hx
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ a✝ ≠ 0

case inr.cons.hy
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ s✝.prod ≠ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
⊢ WellFounded DvdNotUnit

Tactic:
refine RelHomClass.wellFounded
      (RelHom.mk ?_ ?_ : (DvdNotUnit : α → α → Prop) →r ((· < ·) : ℕ∞ → ℕ∞ → Prop)) wellFounded_lt

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
⊢ α → ℕ∞

case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
⊢ ∀ {a b : α}, DvdNotUnit a b → ?refine_1 a < ?refine_1 b
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ r ∣ p.content → ∀ (i : ℕ), r ∣ p.coeff i

Tactic:
intro h i
    apply h.trans (content_dvd_coeff _)

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

Goal state before:
pp: case mp
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
s : Multiset M × Mˣ
hs : s.1 ≤ normalizedFactors y
⊢ ↑s.2 * s.1.prod ∣ y

Tactic:
(unit_associated_one.mul_right s.fst.prod).dvd_iff_dvd_left,

Goal state after:
case mp
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
s : Multiset M × Mˣ
hs : s.1 ≤ normalizedFactors y
⊢ 1 * s.1.prod ∣ y
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
⊢ normUnit X = 1

Tactic:
have := coe_normUnit (R := R) (p := X)

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
this : ↑(normUnit X) = C ↑(normUnit X.leadingCoeff)
⊢ normUnit X = 1
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : DivisionRing R
p : R[X]
hp0 : C (p.coeff 0) ≠ 0
hp : ¬IsUnit (C (p.coeff 0))
h : p.degree ≤ 0
⊢ ¬C (p.coeff 0) = C 0

Tactic:
by simpa using hp0

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ p.primPart.degree ≠ ⊥

Tactic:
rw [Ne, degree_eq_bot]
        apply p.primPart_ne_zero

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

Goal state before:
pp: R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
⊢ eval₂ ϕ α g = 0

Tactic:
obtain ⟨p, hp⟩ := EuclideanDomain.gcd_dvd_right f g
  rw [hp, Polynomial.eval₂_mul, hα, zero_mul]

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

Goal state before:
pp: case refine_3
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : ⟨Associates.mk p, p0_irr⟩ ∈ factors' a ∩ factors' b
⊢ p ∣ b

Tactic:
apply dvd_of_mk_le_mk
    apply dvd_of_mem_factors' (Multiset.mem_inter.mp p0_mem).right
    apply hb

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
⊢ p = {p}.prod

Tactic:
prod_singleton

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
⊢ p = p