mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ WithTop.untopD 1 ↑n = n

Tactic:
rfl

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

Goal state before:
pp: case nil
b b' k : ℕ
h : b ≡ b' [MOD k]
⊢ ofDigits b [] ≡ ofDigits b' [] [MOD k]

Tactic:
rfl

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

Goal state before:
pp: case nil
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
⊢ ofDigits b [] ≡ ofDigits b' [] [ZMOD ↑k]

Tactic:
rfl

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

Goal state before:
pp: case cons
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]
⊢ ofDigits b (d :: L) ≡ ofDigits b' (d :: L) [ZMOD ↑k]

Tactic:
dsimp [ofDigits]
    dsimp [Int.ModEq] at *
    conv_lhs => rw [Int.add_emod, Int.mul_emod, h, ih]
    conv_rhs => rw [Int.add_emod, Int.mul_emod]

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

Goal state before:
pp: case succ
b f : ℕ
ih : ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
n : ℕ
c : Char
tl : List Char
⊢ (if n / b = 0 then (n % b).digitChar :: c :: tl else b.toDigitsCore f (n / b) ((n % b).digitChar :: c :: tl)).length =
    (if n / b = 0 then (n % b).digitChar :: tl else b.toDigitsCore f (n / b) ((n % b).digitChar :: tl)).length + 1

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
⊢ multiplicity a b ≠ 0 ↔ a ∣ b

Tactic:
by
  simp [multiplicity_eq_zero]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_6
inst✝ : DivisionMonoid G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n = 1
h : n = -↑n.natAbs
⊢ x ^ n.natAbs = 1

Tactic:
· rwa [h, zpow_neg, inv_eq_one, zpow_natCast] at hn'

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

Goal state before:
pp: b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
⊢ b + 2 ≠ 1

Tactic:
grind

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

Goal state before:
pp: b : ℕ
hb : 1 < b
a✝ : List ℕ
⊢ a✝ = [] → ∀ x ∈ a✝, x < b

Tactic:
grind

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

Goal state before:
pp: b : ℕ
hb : 1 < b
a✝ : List ℕ
⊢ ((∃ a, a✝ = [a]) ∧ ∀ x ∈ a✝, x < b) ↔ a✝ ∈ Finset.image (fun x ↦ [x]) (Finset.range b)

Tactic:
grind

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
⊢ orderOf 1 = 1

Tactic:
rw [orderOf, ← minimalPeriod_id (x := (1 : G)), ← one_mul_eq_id]

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

Goal state before:
pp: case h_t
p : ℕ
hp : Prime p
q : ℕ
⊢ 1 = ?m.41

Tactic:
rfl

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

Goal state before:
pp: case h_e
p : ℕ
hp : Prime p
q : ℕ
⊢ 0 = ?m.42

Tactic:
rfl

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

Goal state before:
pp: case refine_1.refine_2
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
hL₃ : L ≠ []
⊢ ∀ x ∈ L.tail, x < b

Tactic:
· exact fun x hx ↦ hL₂ _ <| mem_of_mem_tail hx

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : a * 1 = a ^ 2 * v
⊢ False

Tactic:
simp only [sq, mul_assoc, mul_eq_mul_left_iff] at hv

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : 1 = a * v ∨ a = 0
⊢ False
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case hk
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ p ^ n ∣ p ^ n

Tactic:
rfl

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

Goal state before:
pp: d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
h : ∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p
p : ℕ
hp : ¬Prime p
⊢ 0 ≤ 0

Tactic:
rfl

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

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h2 : (n + k).choose k * k ! * n ! = (n + k)!
⊢ ∑ i ∈ Ico 1 b, (n + k) / p ^ i =
    #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}) + (∑ i ∈ Ico 1 b, k / p ^ i + ∑ i ∈ Ico 1 b, n / p ^ i)

Tactic:
multiplicity_choose_aux hp (le_add_left k n)

Goal state after:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h2 : (n + k).choose k * k ! * n ! = (n + k)!
⊢ ∑ i ∈ Ico 1 b, k / p ^ i + ∑ i ∈ Ico 1 b, (n + k - k) / p ^ i +
      #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n + k - k) % p ^ i}) =
    #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}) + (∑ i ∈ Ico 1 b, k / p ^ i + ∑ i ∈ Ico 1 b, n / p ^ i)
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: n k : ℕ
hkn : k ≤ n
| n.choose k

Tactic:
← prod_factorization_pow_eq_self (choose_ne_zero hkn)

Goal state after:
n k : ℕ
hkn : k ≤ n
| (n.choose k).factorization.prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case h
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : n + 1 ≤ p
⊢ p ∉ (n.choose k).factorization.support

Tactic:
rw [Finsupp.mem_support_iff, Classical.not_not, factorization_choose_eq_zero_of_lt hp]

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

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
this : (n + k).choose k * k ! * n ! = (n + k)!
⊢ ↑(∑ i ∈ Ico 1 b, (n + k) / p ^ i) =
    ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) + (↑(∑ i ∈ Ico 1 b, k / p ^ i) + ↑(∑ i ∈ Ico 1 b, n / p ^ i))

Tactic:
multiplicity_choose_aux hp (le_add_left k n)

Goal state after:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
this : (n + k).choose k * k ! * n ! = (n + k)!
⊢ ↑(∑ i ∈ Ico 1 b, k / p ^ i + ∑ i ∈ Ico 1 b, (n + k - k) / p ^ i +
        #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n + k - k) % p ^ i})) =
    ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) + (↑(∑ i ∈ Ico 1 b, k / p ^ i) + ↑(∑ i ∈ Ico 1 b, n / p ^ i))
Module: Mathlib.Algebra.CharP.Frobenius

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p m n : ℕ
inst✝² : ExpChar R p
inst✝¹ : ExpChar S p
x y : R
inst✝ : Algebra R S
r : R
s : S
⊢ (algebraMap R S) ((_root_.frobenius R p) r) * (_root_.frobenius S p) s =
    (algebraMap R S) ((_root_.frobenius R p) r) * (↑↑(_root_.frobenius S p)).toFun s

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
f✝ : R →* S
g : R →+* S
p m n : ℕ
inst✝² : ExpChar R p
inst✝¹ : ExpChar S p
x y : R
inst✝ : Algebra R S
f : R
s : S
⊢ (algebraMap R S) (f ^ p ^ n) * s ^ p ^ n = (algebraMap R S) (f ^ p ^ n) * (↑↑(_root_.iterateFrobenius S p n)).toFun s

Tactic:
rfl

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

Goal state before:
pp: case ofFinsupp
R : Type u
n : ℕ
inst✝ : Semiring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := toFinsupp✝ }.divX.coeff n = { toFinsupp := toFinsupp✝ }.coeff (1 + n)

Tactic:
rfl

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

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
h✝ : p * (n / p) = n
⊢ 0 = 0

Tactic:
rfl

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

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
h✝ : ¬p * (n / p) = n
⊢ 0 = 0

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp1 : p.degree = 1
hm : p.Monic
⊢ p = X - C (-p.coeff 0)

Tactic:
by simpa [hm.leadingCoeff] using eq_X_add_C_of_degree_eq_one hp1

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

Goal state before:
pp: case monomial.monomial.succ.succ
R : Type u
inst✝ : Semiring R
a b : R
m n : ℕ
⊢ (monomial (m + 1 + (n + 1) - 1)) (a * (b * ↑(m + 1))) + (monomial (m + 1 + (n + 1) - 1)) (a * (b * ↑(n + 1))) =
    (monomial (m + 1 - 1 + (n + 1))) (a * (b * ↑(m + 1))) + (monomial (m + 1 + (n + 1 - 1))) (a * (b * ↑(n + 1)))

Tactic:
grind

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
⊢ (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i

Tactic:
wlog h : p.natDegree ≤ n generalizing n

Goal state after:
case inr
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n
⊢ (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i

R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
⊢ (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case isTrue
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h✝ : p = 0
⊢ 0 = 0

Tactic:
rfl

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
hr : C r = 0
⊢ 0 = 0

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
s : Set (Set α)
⊢ ⋯.filter = (FilterBasis.ofSets s).filter

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
a b : R
p : R[X]
⊢ a - b ∣ eval a p - eval b p

Tactic:
suffices X - C b ∣ p - C (p.eval b) by
    simpa only [coe_evalRingHom, eval_sub, eval_X, eval_C]
      using (_root_.map_dvd (evalRingHom a)) this

Goal state after:
R : Type u
inst✝ : CommRing R
a b : R
p : R[X]
⊢ X - C b ∣ p - C (eval b p)
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ i ≤ i

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
x : ℕ → Set α
⊢ (⨅ i, 𝓟 (x i)).IsCountablyGenerated

Tactic:
apply isCountablyGenerated_seq

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst✝¹ : Countable ι
f✝ : ι → Filter α
inst✝ : ∀ (i : ι), (f✝ i).IsCountablyGenerated
s : ι → ℕ → Set α
hs : ∀ (i : ι), (f✝ i).HasAntitoneBasis (s i)
I : Finset (PLift ι)
f : ↑↑I → ℕ
⊢ ⟨↑I, f⟩ ∈ range (Sigma.map SetLike.coe fun x ↦ id)

Tactic:
exact ⟨⟨I, f⟩, rfl⟩

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
l : Filter β
⊢ (∀ (i : ι), Tendsto (eval i ∘ m) l (f i)) ↔ ∀ (i : ι), Tendsto (fun x ↦ m x i) l (f i)

Tactic:
rfl

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

Goal state before:
pp: ι : Sort u_2
α : Type u_3
f : ι → Filter α
s : Set α
hs : s ∈ ⨅ i, f i
⊢ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ i, t i

Tactic:
rw [← iInf_range' (g := (·))] at hs
  let ⟨_, _, V, hVs, _, _, hVU'⟩ := mem_iInf'.1 hs
  use V ∘ rangeFactorization f, fun i ↦ hVs (rangeFactorization f i)
  rw [hVU', ← rangeFactorization_surjective.iInter_comp, comp_def]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
⊢ pi f ⊓ 𝓟 (I.pi s) = ⊥ ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥

Tactic:
← univ_pi_piecewise_univ I,

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
⊢ pi f ⊓ 𝓟 (univ.pi (I.piecewise s fun x ↦ univ)) = ⊥ ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : q.leadingCoeff ∣ p.leadingCoeff
r : R[X]
hr : q = p * r
u : Rˣ
hu : p.leadingCoeff * ↑u = q.leadingCoeff
⊢ q.natDegree ≤ (p * ↑((Units.map ↑C) u)).natDegree

Tactic:
by simpa [natDegree_mul_C] using h₁

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
⊢ (∃ t ∈ g, ∀ᶠ (y : α) in f, ∀ x ∈ t, (x, y) ∈ Prod.swap ⁻¹' s) ↔ ∃ t ∈ g, ∀ᶠ (x : α) in f, ∀ y ∈ t, (x, y) ∈ s

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in map Prod.swap (g ×ˢ f), p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p y.swap

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: case zero
M : Type u_1
inst✝ : AddMonoid M
s : Set M
⊢ {1} = 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: case zero
M : Type u_1
inst✝ : AddMonoid M
s : Set (Multiplicative M)
⊢ {0} = 0

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t = s ×ˢ t

Tactic:
rfl

Goal state after:
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) (map (Prod.mk a) B) = map (f a) B

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
b : β
⊢ map ((fun g ↦ g b) ∘ Prod.mk) f = map (fun a ↦ (a, b)) f

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α → Prop
q : β → Prop
⊢ (f ×ˢ g ⊓ 𝓟 {x | p x.1 ∧ q x.2}).NeBot ↔ (f ×ˢ g ⊓ 𝓟 ({a | p a} ×ˢ {b | q b})).NeBot

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f.coprod g = comap Prod.fst f ⊔ comap Prod.snd g

Tactic:
rfl

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 ∈ la, ∀ W ∈ lc, ∃ U, sᶜ ⊆ U ∧ ∃ V ∈ lb, ∀ (x : α) (y : β), x ∈ U → y ∈ V → f (x, y) ∈ W
h₂ : ∀ W ∈ lc, ∃ U ∈ la, ∀ (x : α) (y : β), x ∈ U → f (x, y) ∈ W
⊢ ∀ W ∈ lc, ∃ V ∈ lb, ∀ (x : α), ∀ y ∈ V, f (x, y) ∈ W

Tactic:
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, ∀ W ∈ lc, ∃ U ∈ la, ∃ V, sᶜ ⊆ V ∧ ∀ (x : α) (y : β), x ∈ U → y ∈ V → f (x, y) ∈ W
h₂ : ∀ W ∈ lc, ∃ V ∈ lb, ∀ (x : α), ∀ y ∈ V, f (x, y) ∈ W
⊢ ∀ W ∈ lc, ∃ U ∈ la, ∀ (x : α) (y : β), x ∈ U → f (x, y) ∈ W

Tactic:
grind

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

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (p : Finset R × R),
    p ∈
        {x ∈ powersetCard (#S - k) S ×ˢ S |
          match x with
          | (T, i) => i ∈ T} ↔
      p.1 ∈ powersetCard (#S - k) S ∧ p.2 ∈ p.1

Tactic:
grind

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

Goal state before:
pp: case left_neg.e_fst
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
r : Finset R × R
hr : r ∈ {x ∈ powersetCard (#S - k) S ×ˢ S | x.2 ∈ x.1}
⊢ insert r.2 (r.1.erase r.2) = r.1

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type ?u.3
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ Associated (a * b) (a * b)

Tactic:
rfl

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

Goal state before:
pp: case empty
M : Type u_4
inst✝ : CommMonoid M
ι : Type u_5
f g : ι → M
h : ∀ i ∈ ∅, f i ~ᵤ g i
⊢ 1 ~ᵤ 1

Tactic:
rfl

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

Goal state before:
pp: case right_neg.e_fst
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
r : Finset R × R
hr : r ∈ {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S | x.2 ∉ x.1}
⊢ (insert r.2 r.1).erase r.2 = r.1

Tactic:
grind

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

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - k) S ×ˢ S |
          match x with
          | (T, i) => i ∈ T}),
    (match a with
      | (T, i) => ∏ a ∈ T.erase i, (X - C a)) =
      match
        match a, ha with
        | (T, i), x => (T.erase i, i) with
      | (T, i) => ∏ a ∈ T, (X - C a)

Tactic:
grind

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

Goal state before:
pp: case hi
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - k) S ×ˢ S |
          match x with
          | (T, i) => i ∈ T}),
    (match a, ha with
      | (T, i), x => (T.erase i, i)) ∈
      {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
        match x with
        | (T, i) => i ∉ T}

Tactic:
grind

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

Goal state before:
pp: case hj
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
          match x with
          | (T, i) => i ∉ T}),
    (match a, ha with
      | (T, i), x => (insert i T, i)) ∈
      {x ∈ powersetCard (#S - k) S ×ˢ S |
        match x with
        | (T, i) => i ∈ T}

Tactic:
grind

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

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (p : Finset R × R),
    p ∈
        {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
          match x with
          | (T, i) => i ∉ T} ↔
      p.1 ∈ powersetCard (#S - (k + 1)) S ∧ p.2 ∈ S \ p.1

Tactic:
grind

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
T : Finset R
hT : T ∈ powersetCard (#S - (k + 1)) S
⊢ #(S \ T) = k + 1

Tactic:
grind

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ (↑k + 1) * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a) =
    ↑(k + 1) * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a)

Tactic:
grind

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
this : DecidableEq (Associates M)
⊢ p.prod ≤ (p + (q - p)).prod

Tactic:
suffices p.prod * 1 ≤ p.prod * (q - p).prod by simpa

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
this : DecidableEq (Associates M)
⊢ p.prod * 1 ≤ p.prod * (q - p).prod
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ p.roots = if h : p = 0 then ∅ else Classical.choose ⋯

Tactic:
rfl

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

Goal state before:
pp: σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
⊢ {d | (weight w) d < n} ⊆ {d | (weight w) d ≤ n}

Tactic:
grind

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

Goal state before:
pp: σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
⊢ {d | (weight w) d = n} ⊆ {d | (weight w) d ≤ n}

Tactic:
grind

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

Goal state before:
pp: σ : Type u_1
inst✝ : Finite σ
n : ℕ
⊢ {f | degree f < n} ⊆ {f | degree f ≤ n}

Tactic:
grind

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

Goal state before:
pp: σ : Type u_1
inst✝ : Finite σ
n : ℕ
⊢ {f | degree f = n} ⊆ {f | degree f ≤ n}

Tactic:
grind

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

Goal state before:
pp: σ : Type u_5
g f : σ →₀ ℕ
hgf : g ≤ g + f
IH : degree g ≤ degree (g + f) → ∃ g_1 ≤ g + f, degree g_1 = degree g
hn : degree g + 1 ≤ degree (g + f)
i : σ
hi : i ∈ f.support
⊢ 1 ≤ f i

Tactic:
grind

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

Goal state before:
pp: σ : Type u_5
s t : Set ℕ
f : σ →₀ ℕ
m : ℕ
hm : m ∈ s
n : ℕ
hn : n ∈ t
e : m + n = degree f
⊢ m ≤ degree f

Tactic:
grind

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

Goal state before:
pp: case succ.refine_1
α : Type u_5
s : Set α
n : ℕ
ih : n • (fun x ↦ single x 1) '' s = {x | degree x = n ∧ ↑x.support ⊆ s}
⊢ ∀ (b : α →₀ ℕ),
    degree b = n →
      (∀ (x : α), ¬b x = 0 → x ∈ s) → ∀ a ∈ s, degree b = n ∧ ∀ (x : α), (b x = 0 → ¬(single a 1) x = 0) → x ∈ s

Tactic:
grind

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
⊢ (X ^ n).roots = n • {0}

Tactic:
by
  rw [roots_pow, roots_X]

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

Goal state before:
pp: case mp
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
⊢ p ∈ normalizedFactors x → Prime p ∧ p ∣ x

Tactic:
intro h
    exact ⟨prime_of_normalized_factor p h, dvd_of_mem_normalizedFactors 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]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : ↑(#S) = p.degree
⊢ p.degree ≤ ↑(#S)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x✝ : Associates α
hx : ¬x✝ = 0
x : Associates α
⊢ x = id x

Tactic:
rfl

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝ : CommMonoid β
f : α → β
n : ℕ
s : Set α
⊢ (f '' s) ^ n = (fun x ↦ x.prod fun x1 x2 ↦ f x1 ^ x2) '' {x | degree x = n ∧ ↑x.support ⊆ s}

Tactic:
classical
  suffices ∀ (s : Set (α →₀ ℕ)), ((·.prod (f · ^ ·)) '' s) ^ n = (·.prod (f · ^ ·)) '' (n • s) by
    simp [← nsmul_single_one_image, ← this, Set.image_image]
  intro s
  refine (Set.image_pow (⟨⟨(·.prod (f · ^ ·)) ∘ Multiplicative.toAdd, by simp⟩,
    by simp [Finsupp.prod_add_index, pow_add]⟩ : Multiplicative (α →₀ ℕ) →* β) _ _).symm.trans ?_
  simp [-Function.comp_apply, Set.image_comp, show Multiplicative.toAdd '' s = s from
    Set.image_id _]

Goal state after: