mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p : ℕ
pp : ¬Prime p
⊢ 0 < p ^ n.factorization p

Tactic:
else

Goal state after:
n p : ℕ
pp : ¬Prime p
⊢ 0 < p ^ n.factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p : ℕ
⊢ 0 < p ^ n.factorization p

Tactic:
by
  if pp : p.Prime then simp [Nat.pow_pos pp.pos] else simp [pp]

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

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

Tactic:
else

Goal state after:
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ 0 < n / p ^ n.factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b p : ℕ
ha : ¬a = 0
⊢ a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)

Tactic:
else

Goal state after:
a b p : ℕ
ha : ¬a = 0
⊢ a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
H : Type u_6
inst✝ : Monoid H
f : G →* H
hf : Injective ⇑f
x : G
⊢ ∀ (n : ℕ), True

Tactic:
forall_const

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

Goal state before:
pp: a b p : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)

Tactic:
else

Goal state after:
a b p : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p b : ℕ
hb : n ≤ p ^ b
hn : ¬n = 0
⊢ n.factorization p ≤ b

Tactic:
else

Goal state after:
n p b : ℕ
hb : n ≤ p ^ b
hn : ¬n = 0
⊢ n.factorization p ≤ b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p b : ℕ
hb : n ≤ p ^ b
hn : ¬n = 0
pp : ¬Prime p
⊢ n.factorization p ≤ b

Tactic:
else

Goal state after:
n p b : ℕ
hb : n ≤ p ^ b
hn : ¬n = 0
pp : ¬Prime p
⊢ n.factorization p ≤ b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p : ℕ
hn : ¬n = 0
⊢ (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization

Tactic:
else

Goal state after:
n p : ℕ
hn : ¬n = 0
⊢ (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p : ℕ
hn : ¬n = 0
pp : ¬Prime p
⊢ (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization

Tactic:
else

Goal state after:
n p : ℕ
hn : ¬n = 0
pp : ¬Prime p
⊢ (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
⊢ d ∣ n / p ^ n.factorization p

Tactic:
else

Goal state after:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
⊢ d ∣ n / p ^ n.factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
⊢ d ∣ n / p ^ n.factorization p

Tactic:
else

Goal state after:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
⊢ d ∣ n / p ^ n.factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
q : ℕ
hqp : ¬q = p
⊢ d.factorization q ≤ (Finsupp.erase p n.factorization) q

Tactic:
else

Goal state after:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
q : ℕ
hqp : ¬q = p
⊢ d.factorization q ≤ (Finsupp.erase p n.factorization) q
Module: Mathlib.Data.Nat.Choose.Factorization

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

Tactic:
Classical.not_not,

Goal state after:
case h
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : n + 1 ≤ p
⊢ (n.choose k).factorization p = 0
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : ¬Prime a
⊢ a ∣ b

Tactic:
else

Goal state after:
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : ¬Prime a
⊢ a ∣ b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : ¬Prime b
⊢ a ∣ b

Tactic:
else

Goal state after:
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : ¬Prime b
⊢ a ∣ b
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ ∑ x_1 ∈ cons (p ^ n) (cons 0 (Ioo 0 (p ^ n)) ⋯) ⋯, x ^ x_1 * y ^ (p ^ n - x_1) * ↑((p ^ n).choose x_1) =
    x ^ p ^ n + y ^ p ^ n + ∑ x_1 ∈ Ioo 0 (p ^ n), x ^ x_1 * y ^ (p ^ n - x_1) * ↑((p ^ n).choose x_1)

Tactic:
simp [-cons_eq_insert, add_assoc]

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

Goal state before:
pp: n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ ¬¬FiniteMultiplicity p (p * n)!

Tactic:
Classical.not_not,

Goal state after:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ FiniteMultiplicity p (p * n)!
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1

Tactic:
rw [← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast, pow_orderOf_eq_one, one_zpow]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
x y : G
α : Type u_6
inst✝ : MulAction G α
hx : x ∈ zpowers y
a : α
hs : y • a = a
⊢ x • a = a

Tactic:
obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp hx
  rw [← MulAction.toPerm_apply, ← MulAction.toPermHom_apply, map_zpow _ y k,
    MulAction.toPermHom_apply]
  exact Function.IsFixedPt.perm_zpow (by exact hs) k

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * b).factorization = a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization

Tactic:
factorization_mul ha hb

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorization + b.factorization = a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
hn₀ : n ≠ 0
⊢ (m.primeFactors ∪ n.primeFactors).prod f * (m.primeFactors ∩ n.primeFactors).prod f =
    m.primeFactors.prod f * n.primeFactors.prod f

Tactic:
Finset.prod_union_inter

Goal state after:
case inr.inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
hn₀ : n ≠ 0
⊢ (∏ x ∈ m.primeFactors, f x) * ∏ x ∈ n.primeFactors, f x = m.primeFactors.prod f * n.primeFactors.prod f
Module: Mathlib.Algebra.MonoidAlgebra.Division

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

Tactic:
ext g'
  simp only [of'_apply, coeff_zero, Finsupp.coe_zero, Pi.zero_apply]
  obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
  · rw [coeff_modOf_self_add]
  · rw [coeff_modOf_of_not_exists_add _ _ _ h, coeff_single_mul_of_forall_add_ne]
    simpa [eq_comm] using h

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝¹ : LeftCancelMonoid M
inst✝ : Finite M
S : Set M
hS1 : S.Nonempty
hS2 : S * S = S
pow_mem : ∀ a ∈ S, ∀ (n : ℕ), a ^ (n + 1) ∈ S
⊢ 1 ∈ S

Tactic:
obtain ⟨a, ha⟩ := hS1

Goal state after:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝¹ : LeftCancelMonoid M
inst✝ : Finite M
S : Set M
hS2 : S * S = S
pow_mem : ∀ a ∈ S, ∀ (n : ℕ), a ^ (n + 1) ∈ S
a : M
ha : a ∈ S
⊢ 1 ∈ S
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case refine_2.inl.inr
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
p q : R[X]
hp : p.natDegree = 0
hq : M q
⊢ (p + q).natDegree = 0 ∨ M (p + q)

Tactic:
refine Or.inr ?_
      rw [eq_C_of_natDegree_eq_zero hp]
      exact h_C_add hq

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a b : R
f g : R[X]
h_add_left : f.coeff n = a
h_add_right : g.coeff n = b
⊢ (f + g).coeff n = a + b

Tactic:
subst ‹_› ‹_›; apply coeff_add

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
rw [hq, mul_zero, trailingDegree_zero, add_top]

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

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

Tactic:
contrapose! hn

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ Prime X

Tactic:
convert! prime_X_sub_C (0 : R)

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ X = X - C 0
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:
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: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ derivative (C a * X ^ n) = C (a * ↑n) * X ^ (n - 1)

Tactic:
rw [C_mul_X_pow_eq_monomial, C_mul_X_pow_eq_monomial, derivative_monomial]

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] (s • p) = s • (⇑derivative)^[k] p

Tactic:
induction k generalizing p with

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ -C ↑h.unit⁻¹ * (X - C a) + C ↑h.unit⁻¹ * (X - C b) = 1

Tactic:
by
    rw [neg_mul_comm, ← left_distrib, neg_add_eq_sub, sub_sub_sub_cancel_left, ← C_sub, ← C_mul]
    rw [← C_1]
    congr
    exact h.val_inv_mul

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

Goal state before:
pp: case succ
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k)) f) = f ^ p ^ k
⊢ map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1))) f) = f ^ p ^ (k + 1)

Tactic:
symm
    conv_lhs => rw [pow_succ, pow_mul, ← n_ih]
    simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
⊢ IsLocalHom (expand R p)

Tactic:
refine ⟨fun f hf1 => ?_⟩

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit ((expand R p) f)
⊢ IsUnit f
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
k : ℕ
⊢ (⇑derivative)^[k] (map f p) = map f ((⇑derivative)^[k] p)

Tactic:
induction k generalizing p with

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ i ∈ range n.succ, (n + 1).choose (i + 1) • ((⇑derivative)^[n + 1 - (i + 1)] p * (⇑derivative)^[i + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q) =
    ∑ k ∈ range n.succ, n.succ.choose (k + 1) • ((⇑derivative)^[n.succ - (k + 1)] p * (⇑derivative)^[k + 1] q) +
      n.succ.choose 0 • ((⇑derivative)^[n.succ - 0] p * (⇑derivative)^[0] q)

Tactic:
Nat.choose_zero_right,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ i ∈ range n.succ, (n + 1).choose (i + 1) • ((⇑derivative)^[n + 1 - (i + 1)] p * (⇑derivative)^[i + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q) =
    ∑ k ∈ range n.succ, n.succ.choose (k + 1) • ((⇑derivative)^[n.succ - (k + 1)] p * (⇑derivative)^[k + 1] q) +
      1 • ((⇑derivative)^[n.succ - 0] p * (⇑derivative)^[0] q)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ.e_a.refine_2
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ n.choose 0 • ((⇑derivative)^[n - 0 + 1] p * (⇑derivative)^[0] q) = 1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)

Tactic:
Nat.choose_zero_right,

Goal state after:
case succ.e_a.refine_2
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ 1 • ((⇑derivative)^[n - 0 + 1] p * (⇑derivative)^[0] q) = 1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : X - C a ∣ p
⊢ p.IsRoot a

Tactic:
by
    rwa [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval, ← C_0,
      C_inj] at h

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

Goal state before:
pp: α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ∃ I_1,
    I_1.Finite ∧
      ∃ V_1, (∀ (i : ι), V_1 i ∈ s i) ∧ (∀ i ∉ I_1, V_1 i = univ) ∧ ⋂ i, V i = ⋂ x, V_1 ↑x ∧ ⋂ i, V i = ⋂ i, V_1 i

Tactic:
refine ⟨I, If, fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ, fun i => ?_, fun i hi => ?_, ?_⟩

Goal state after:
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

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.Filter.Finite

Goal state before:
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:
simp only [iInter_dite, biInter_eq_iInter, dif_pos (Subtype.coe_prop _), Subtype.coe_eta,
      iInter_univ, inter_univ, true_and]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
⊢ derivative (p.comp q) = derivative q * (derivative p).comp q

Tactic:
induction p using Polynomial.induction_on'
  · simp [*, mul_add]
  · simp only [derivative_pow, derivative_mul, monomial_comp, derivative_monomial, derivative_C,
      zero_mul, C_eq_natCast, zero_add, map_mul]
    ring

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

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

Tactic:
rw [sup_comm a, inf_comm]
  exact boundary_le_boundary_sup_sup_boundary_inf_left

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

Goal state before:
pp: α : Type u_2
l : Filter α
inst✝ : l.IsCountablyGenerated
h : cofinite ≤ l
⊢ l.kerᶜ.Countable

Tactic:
rcases exists_antitone_basis l with ⟨s, hs⟩
  simp only [hs.ker, iInter_true, compl_iInter]
  exact countable_iUnion fun n ↦ Set.Finite.countable <| h <| hs.mem _

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_4
s : (i : ι) → Set (α i)
l : (i : ι) → Filter (α i)
h : ∀ (i : ι), s i ∈ l i
hfin : ∀ᶠ (i : ι) in cofinite, s i = univ
a : (i : ι) → α i
ha : a ∈ {x | s x = univ}ᶜ.pi s
i : ι
a✝ : i ∈ univ
hi : ¬s i = univ
⊢ a i ∈ s i

Tactic:
else

Goal state after:
ι : Type u_1
α : ι → Type u_4
s : (i : ι) → Set (α i)
l : (i : ι) → Filter (α i)
h : ∀ (i : ι), s i ∈ l i
hfin : ∀ᶠ (i : ι) in cofinite, s i = univ
a : (i : ι) → α i
ha : a ∈ {x | s x = univ}ᶜ.pi s
i : ι
a✝ : i ∈ univ
hi : ¬s i = univ
⊢ a i ∈ s i
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case mpr
α : Type u_2
f : Filter α
h : f.kerᶜ ∈ f
⊢ f.ker = ∅

Tactic:
rw [eq_empty_iff_forall_notMem]

Goal state after:
case mpr
α : Type u_2
f : Filter α
h : f.kerᶜ ∈ f
⊢ ∀ (x : α), x ∉ f.ker
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: case mp
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ Prod.map (fun x ↦ b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ → (b', i') ∈ {b} ×ˢ univ

Tactic:
rintro ⟨⟨a'', i''⟩, _, h₂, h₃⟩
    simp

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] (p.comp (1 - X)) = (-1) ^ k * ((⇑derivative)^[k] p).comp (1 - X)

Tactic:
induction k generalizing p with

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] (p.comp (1 - X)) = (-1) ^ k * ((⇑derivative)^[k] p).comp (1 - X)

Tactic:
induction k generalizing p with
  | zero => simp
  | succ k ih => simp [ih (derivative p), derivative_comp, pow_succ]

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

Goal state before:
pp: σ : Type u_1
R : Type u_5
inst✝² : AddCommMonoid R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
⊢ f s ≤ degree f

Tactic:
by
  by_cases h : s ∈ f.support
  · exact Finset.single_le_sum_of_canonicallyOrdered h
  · simp only [notMem_support_iff] at h
    simp only [h, zero_le]

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

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

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

Tactic:
· rw [mul_right_comm _ _ q, mul_assoc, ← Multiset.prod_cons, Multiset.cons_erase hq, ← hu,
          mul_comm, mul_comm p _, mul_assoc]
        simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
⊢ Fintype { x // x ∣ y }

Tactic:
by
  haveI : Nontrivial M := ⟨⟨y, 0, hy⟩⟩
  haveI : StrongNormalizationMonoid M := UniqueFactorizationMonoid.strongNormalizationMonoid
  haveI := Classical.decEq M
  haveI := Classical.decEq (Associates M)
  -- We'll show `fun (u : Mˣ) (f ⊆ factors y) ↦ u * Π f` is injective
  -- and has image exactly the divisors of `y`.
  refine
    Fintype.subtype
      (((normalizedFactors y).powerset.toFinset ×ˢ (Finset.univ : Finset Mˣ)).image fun s =>
        (s.snd : M) * s.fst.prod)
      fun x => ?_
  simp only [Finset.mem_image, Finset.mem_product, Finset.mem_univ, and_true,
    Multiset.mem_toFinset, Multiset.mem_powerset]
  constructor
  · rintro ⟨s, hs, rfl⟩
    rw [(unit_associated_one.mul_right s.fst.prod).dvd_iff_dvd_left, one_mul,
      ← (prod_normalizedFactors hy).dvd_iff_dvd_right]
    exact Multiset.prod_dvd_prod_of_le hs
  · rintro (h : x ∣ y)
    have hx : x ≠ 0 := by
      refine mt (fun hx => ?_) hy
      rwa [hx, zero_dvd_iff] at h
    obtain ⟨u, hu⟩ := prod_normalizedFactors hx
    refine ⟨⟨normalizedFactors x, u⟩, ?_, (mul_comm _ _).trans hu⟩
    exact (dvd_iff_normalizedFactors_le_normalizedFactors hx hy).mp h

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

Goal state before:
pp: case coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ (∃ a ∈ a✝, ↑a = 0) ↔ False

Tactic:
iff_false,

Goal state after:
case coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ ¬∃ a ∈ a✝, ↑a = 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : ¬q = 0
⊢ map f (p / q) = map f p / map f q

Tactic:
else

Goal state after:
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : ¬q = 0
⊢ map f (p / q) = map f p / map f q
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
⊢ IsCoprime (map f p) (map f q) ↔ IsCoprime p q

Tactic:
rw [← EuclideanDomain.gcd_isUnit_iff, ← EuclideanDomain.gcd_isUnit_iff, gcd_map, isUnit_map]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
sC : 0 < s.natDegree
hcancel : (r.cancelLeads s).natDegree < Nat.find con
⊢ False

Tactic:
apply Nat.find_min con hcancel

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
sC : 0 < s.natDegree
hcancel : (r.cancelLeads s).natDegree < Nat.find con
⊢ ∃ s_1, s_1.natDegree = (r.cancelLeads s).natDegree ∧ (p ∣ s_1 ∧ q ∣ s_1) ∧ ¬r ∣ s_1