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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
p a b : α
⊢ min (emultiplicity p a) (emultiplicity p b) ≤ emultiplicity p (a + b)

Tactic:
cases hm : min (emultiplicity p a) (emultiplicity p b)

Goal state after:
case top
α : Type u_1
inst✝ : Semiring α
p a b : α
hm : min (emultiplicity p a) (emultiplicity p b) = ⊤
⊢ ⊤ ≤ emultiplicity p (a + b)

case coe
α : Type u_1
inst✝ : Semiring α
p a b : α
a✝ : ℕ
hm : min (emultiplicity p a) (emultiplicity p b) = ↑a✝
⊢ ↑a✝ ≤ emultiplicity p (a + b)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
a b : α
x✝ : ℕ
⊢ a ^ (x✝ + 1) ∣ -b ↔ a ^ (x✝ + 1) ∣ b

Tactic:
simp only [dvd_neg]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
rw [orderOf, minimalPeriod_eq_one_iff_isFixedPt, IsFixedPt, mul_one]

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

Goal state before:
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
⊢ ∑ i ∈ Finset.range b, ∑ x ∈ fixedLengthDigits hb l, (i + x.sum) = (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
Finset.sum_comm

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
⊢ ∑ y ∈ fixedLengthDigits hb l, ∑ x ∈ Finset.range b, (x + y.sum) = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
eq_comm,

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : ¬FiniteMultiplicity p (a * b)
⊢ emultiplicity p a + emultiplicity p b = ⊤
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
· rw [pow_dvd_pow_iff h0 hu]
    apply Nat.not_succ_le_self

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

Goal state before:
pp: case neg
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ n.factorization p < n

Tactic:
· simpa only [factorization_eq_zero_of_not_prime n pp] using! hn.bot_lt

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
eq_comm,

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

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

Tactic:
eq_comm,

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

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

Tactic:
eq_comm,

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

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : IsMulTorsionFree G
g : G
ha : ¬g = 1
⊢ orderOf g ≤ 1

Tactic:
← isOfFinOrder_iff_eq_one,

Goal state after:
case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : IsMulTorsionFree G
g : G
ha : ¬IsOfFinOrder g
⊢ orderOf g ≤ 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G₀ : Type u_6
inst✝¹ : GroupWithZero G₀
inst✝ : Finite G₀
a : G₀
⊢ orderOf a = 0 ↔ a = 0

Tactic:
have : Finite G₀ˣ := .of_injective _ Units.val_injective
  simp [isOfFinOrder_iff_isUnit]

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

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
this : CharZero R
⊢ False

Tactic:
exact absurd Nat.cast_injective (not_injective_infinite_finite ((↑) : ℕ → R))

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 % card G) = a ^ n

Tactic:
eq_comm,

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

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

Tactic:
eq_comm,

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

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

Tactic:
eq_comm,

Goal state after:
G : Type u_6
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ n = a ^ (n % Nat.card G)
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
eq_comm,

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

Goal state before:
pp: case hfg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ n.factorization.support
⊢ (fun x1 x2 ↦ x1 ^ x2) p (n.factorization p) = p ^ padicValNat p n

Tactic:
simp [factorization_def n (prime_of_mem_primeFactors hp)]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case mp
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
g : G
x : k[G]
⊢ of' k G g * x %ᵒᶠ g = 0

Tactic:
of'_mul_modOf

Goal state after:
case mp
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
g : G
x : k[G]
⊢ 0 = 0
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case refine_2
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
h : n.primeFactors ⊆ k.primeFactors
⊢ n ∣ k ^ n

Tactic:
grw [dvd_prod_primeFactors_pow_self hn, prod_dvd_prod_of_subset _ _ _ h, prod_primeFactors_dvd]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case mp
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
H : ↑p = 0
h : ↑(n % p) = 0
⊢ n % p = 0

Tactic:
apply hR _ (Nat.mod_lt _ _) h

Goal state after:
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
H : ↑p = 0
h : ↑(n % p) = 0
⊢ 0 < p
Module: Mathlib.Algebra.Polynomial.Expand

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

Tactic:
simp only [expand_eq_sum]

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ (f.sum fun e a ↦ C a * (X ^ p) ^ e).coeff n = if p ∣ n then f.coeff (n / p) else 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
⊢ (p /ₘ q).degree ≤ p.degree

Tactic:
by simp only [hp0, zero_divByMonic, le_refl]

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

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

Tactic:
pow_succ'

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
⊢ (∀ (x_1 : R[X]), ¬(x_1 ≠ 0 ∧ (aeval x) x_1 = 0)) ↔ ∀ (p : R[X]), (aeval x) p = 0 → p = 0

Tactic:
congr! 1

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
a✝ : R[X]
⊢ ¬(a✝ ≠ 0 ∧ (aeval x) a✝ = 0) ↔ (aeval x) a✝ = 0 → a✝ = 0
Module: Mathlib.RingTheory.Algebraic.Defs

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ S.IsAlgebraic ↔ Algebra.IsAlgebraic R ↥S

Tactic:
delta Subalgebra.IsAlgebraic
  rw [Subtype.forall', Algebra.isAlgebraic_def]
  refine forall_congr' fun x => exists_congr fun p => and_congr Iff.rfl ?_
  have h : Function.Injective S.val := Subtype.val_injective
  conv_rhs => rw [← h.eq_iff, map_zero]
  rw [← aeval_algHom_apply, S.val_apply]

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

Goal state before:
pp: case inr.refine_1
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✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ p.coeff (n + 1) + a * ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i =
    ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i

Tactic:
eq_comm,

Goal state after:
case inr.refine_1
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✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i =
    p.coeff (n + 1) + a * ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr.refine_1.e_a.refine_2
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✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ a ^ (i - (n + 1)) * p.coeff i = a ^ (i - (n + 1 + 1) + 1) * p.coeff i

Tactic:
eq_comm,

Goal state after:
case inr.refine_1.e_a.refine_2
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✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ a ^ (i - (n + 1 + 1) + 1) * p.coeff i = a ^ (i - (n + 1)) * p.coeff i
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 : 0 = (m + 1) • p.coeff (m + 1)
⊢ False

Tactic:
eq_comm,

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 : (m + 1) • p.coeff (m + 1) = 0
⊢ False
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α : Type u_1
ι' : Sort u_5
inst✝ : Countable ι'
x : ι' → Set α
⊢ (⨅ i, 𝓟 (x i)).IsCountablyGenerated

Tactic:
use range x, countable_range x

Goal state after:
case right
α : Type u_1
ι' : Sort u_5
inst✝ : Countable ι'
x : ι' → Set α
⊢ ⨅ i, 𝓟 (x i) = generate (range x)
Module: Mathlib.Order.Filter.Finite

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

Tactic:
refine ⟨exists_iInter_of_mem_iInf, ?_⟩

Goal state after:
ι : Sort u_2
inst✝ : Finite ι
α : Type u_3
f : ι → Filter α
s : Set α
⊢ (∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ i, t i) → s ∈ ⨅ i, f i
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
hgu : IsUnit g
⊢ p.degree = 1

Tactic:
rw [hg, degree_mul, degree_X_sub_C, degree_eq_zero_of_isUnit hgu, add_zero]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ f ×ˢ g → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s

Tactic:
rintro ⟨t₁, ⟨s₁, hs₁, hts₁⟩, t₂, ⟨s₂, hs₂, hts₂⟩, rfl⟩
    exact ⟨s₁, hs₁, s₂, hs₂, fun p ⟨h, h'⟩ => ⟨hts₁ h, hts₂ h'⟩⟩

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

Goal state before:
pp: case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
hd : 0 < p.degree
⊢ 1 ≤ p.degree

Tactic:
Nat.WithBot.one_le_iff_zero_lt

Goal state after:
case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
hd : 0 < p.degree
⊢ 0 < p.degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = p.leadingCoeff * u.coeff 0
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
⊢ p = p * u

Tactic:
eq_comm,

Goal state after:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff * u.coeff 0 = p.leadingCoeff
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
⊢ p = p * u
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g : Filter β
⊢ (f₁ ⊔ f₂) ×ˢ g = f₁ ×ˢ g ⊔ f₂ ×ˢ g

Tactic:
by
  simp only [prod_eq_inf, comap_sup, inf_sup_right]

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
⊢ (univ.pi fun i ↦ f i '' (I, s).1.piecewise (fun i ↦ id ((I, s).2 i)) (fun x ↦ univ) i) ∈ pi fun i ↦ map (f i) (l i)

Tactic:
refine univ_pi_mem_pi (fun i ↦ ?_) ?_

Goal state after:
case refine_1
ι : 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
i : ι
⊢ f i '' (I, s).1.piecewise (fun i ↦ id ((I, s).2 i)) (fun x ↦ univ) i ∈ map (f i) (l i)

case refine_2
ι : 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
⊢ ∀ᶠ (i : ι) in cofinite, f i '' (I, s).1.piecewise (fun i ↦ id ((I, s).2 i)) (fun x ↦ univ) i = univ
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
p : Finset ι
f : ι → M
⊢ ∏ i ∈ p, Associates.mk (f i) = Associates.mk (∏ i ∈ p, f i)

Tactic:
Finset.prod_eq_multiset_prod,

Goal state after:
ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
p : Finset ι
f : ι → M
⊢ (Multiset.map (fun i ↦ Associates.mk (f i)) p.val).prod = Associates.mk (∏ i ∈ p, f i)
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:
simpa using roots_X_sub_C (-r)

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

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

Tactic:
eq_comm,

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : a = 0
⊢ p ∣ a

Tactic:
rw [hcases]

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : a = 0
⊢ p ∣ 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : 0 < n
⊢ 1 ∈ nthRootsFinset n 1

Tactic:
rw [mem_nthRootsFinset hn, one_pow]

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

Goal state before:
pp: T : Type w
inst✝⁸ : CommRing T
p : T[X]
inst✝⁷ : IsDomain T
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : Module.IsTorsionFree T S'
f : S →ₐ[T] S'
⊢ Set.MapsTo (⇑f) (p.rootSet S) (p.rootSet S')

Tactic:
refine rootSet_maps_to' (fun h₀ => ?_) f
  obtain rfl : p = 0 :=
    map_injective _ (FaithfulSMul.algebraMap_injective T S') (by rwa [Polynomial.map_zero])
  exact Polynomial.map_zero _

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

Goal state before:
pp: case top.coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ⊤ = prod ↑a✝
⊢ ⊤ = ↑a✝

Tactic:
eq_comm,

Goal state after:
case top.coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ⊤ = prod ↑a✝
⊢ ↑a✝ = ⊤
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hirr : Irreducible p
hdeg : p.natDegree ≠ 1
hroots : ¬p.roots = 0
x : R
hx : x ∈ p.roots
⊢ False

Tactic:
exact hdeg <| natDegree_eq_of_degree_eq_some <|
    degree_eq_one_of_irreducible_of_root hirr (mem_roots'.mp hx).right

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

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
⊢ ∀ (a : R[X]), a / 0 = 0

Tactic:
simp [div_def]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton α
a : Associates α
this : Subsingleton (Associates α)
⊢ a.factors = ⊤

Tactic:
convert! factors_zero

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - C a ∣ f /ₘ (X - C a)
key : f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
u : K[X]
hu : f /ₘ (X - C a) = (X - C a) * u
⊢ X - C a ∣ derivative f

Tactic:
rw [← key, hu, ← mul_add (X - C a) u _]

Goal state after:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - C a ∣ f /ₘ (X - C a)
key : f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
u : K[X]
hu : f /ₘ (X - C a) = (X - C a) * u
⊢ X - C a ∣ (X - C a) * (u + derivative ((X - C a) * u))
Module: Mathlib.Algebra.Central.End

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∃ y, ↑g ∘ₗ (y • 1) = ↑f) ↔ ∃ α, ⇑f = α • ⇑g

Tactic:
eq_comm,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∃ y, ↑f = ↑g ∘ₗ (y • 1)) ↔ ∃ α, ⇑f = α • ⇑g
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_ne : (aeval x) p.divX ≠ 0
⊢ x = ((aeval x) p - (algebraMap K L) (p.coeff 0)) / (aeval x) p.divX

Tactic:
eq_comm,

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_ne : (aeval x) p.divX ≠ 0
⊢ ((aeval x) p - (algebraMap K L) (p.coeff 0)) / (aeval x) p.divX = x