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

Goal state before:
pp: σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.coeff.support
this : ∑ i ∈ d.support, d i * n ≤ m * n
⊢ ∑ i ∈ d.support, ((fun n e ↦ f n ^ e) i (d i)).natDegree ≤ m * n

Tactic:
apply (Finset.sum_le_sum _).trans this

Goal state after:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.coeff.support
this : ∑ i ∈ d.support, d i * n ≤ m * n
⊢ ∀ i ∈ d.support, ((fun n e ↦ f n ^ e) i (d i)).natDegree ≤ d i * n
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a : ℤ
⊢ a % n = 0 % n ↔ n ∣ a

Tactic:
zero_emod,

Goal state after:
n a : ℤ
⊢ a % n = 0 ↔ n ∣ a
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
⊢ a + b ≡ b [ZMOD n] ↔ n ∣ a

Tactic:
add_modEq_right_iff

Goal state after:
n a b : ℤ
⊢ n ∣ a ↔ n ∣ a
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case mp
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
⊢ x ∈ ker (Quotient.lift I f H) → x ∈ map (Quotient.mk I) (ker f)

Tactic:
intro hx

Goal state after:
case mp
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
hx : x ∈ ker (Quotient.lift I f H)
⊢ x ∈ map (Quotient.mk I) (ker f)
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case mpr
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
⊢ x ∈ map (Quotient.mk I) (ker f) → x ∈ ker (Quotient.lift I f H)

Tactic:
intro hx

Goal state after:
case mpr
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
hx : x ∈ map (Quotient.mk I) (ker f)
⊢ x ∈ ker (Quotient.lift I f H)
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: case inr
α : Type u_1
inst✝ : GroupWithZero α
h✝ : Infinite { a // a ≠ 0 }
⊢ Nat.card ({ a // a = 0 } ⊕ { a // ¬a = 0 }) - 1 = Nat.card { a // a ≠ 0 }

Tactic:
· rw [Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_tsub]

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : Field R
inst✝⁶ : StarRing R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : StarModule R A
inst✝¹ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R ↑s) :=
  (unitization s).codRestrict (StarAlgebra.adjoin R ↑s) ⋯
x✝ : ↥s
⊢ ((StarAlgebra.adjoin R ↑s).subtype.comp starAlgHom) ↑x✝ = ↑x✝

Tactic:
by simp [starAlgHom]

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

Goal state before:
pp: n : ℕ
⊢ n = 1 ↔ ∀ (p : ℕ), Prime p → ¬p ∣ n

Tactic:
by
  simpa using not_iff_not.mpr ne_one_iff_exists_prime_dvd

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (ts is : List α), map (map f) (ts.permutationsAux is) = (map f ts).permutationsAux (map f is)

Tactic:
refine permutationsAux.rec (by simp) ?_
  introv IH1 IH2; rw [map] at IH2
  simp only [foldr_permutationsAux2, map_append, map, map_map_permutationsAux2, permutations,
    flatMap_map, IH1, append_assoc, permutationsAux_cons, flatMap_cons, ← IH2, map_flatMap]

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
a b : α
l : List α
⊢ l ~ [a, b] ↔ l = [a, b] ∨ l = [b, a]

Tactic:
by
  have : [a, b].permutations = [[a, b], [b, a]] := by cbv
  grind [=_ mem_permutations]

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ minimalPeriod g x.2 ∣ (minimalPeriod f x.1).lcm (minimalPeriod g x.2)

Tactic:
exact Nat.dvd_lcm_right _ _

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
H : Subgroup G
ω : Quotient (orbitRel G X)
q : orbitRel.Quotient ↥H ↑(orbitRel.Quotient.orbit ω)
a b : ↑(orbitRel.Quotient.orbit ω)
h : (orbitRel ↥H ↑(orbitRel.Quotient.orbit ω)) a b
⊢ ⟦⟨↑a, ⋯⟩⟧ = ⟦⟨↑b, ⋯⟩⟧

Tactic:
simp only [← Quotient.eq, orbitRel.Quotient.subgroup_quotient_eq_iff] at h
      simp only [Quotient.eq] at h ⊢
      exact h

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : K.Normal
⊢ K.relIndex (K ⊔ H) = K.relIndex H

Tactic:
rw [sup_comm, relIndex_sup_right]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.relIndex K = 2 ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b * a ∈ H ∨ b ∈ H

Tactic:
Subgroup.relIndex,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (H.subgroupOf K).index = 2 ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b * a ∈ H ∨ b ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.relIndex K = 2 ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a * b ∈ H ∨ b ∈ H

Tactic:
Subgroup.relIndex,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (H.subgroupOf K).index = 2 ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a * b ∈ H ∨ b ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ (-↑n₁) * a ^ ↑n₂ ∈ H
⊢ a ^ (n₂ - n₁) ∈ H

Tactic:
← zpow_add,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ (-↑n₁ + ↑n₂) ∈ H
⊢ a ^ (n₂ - n₁) ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.FiniteIndex
⊢ H.IsFiniteRelIndex K

Tactic:
← isFiniteRelIndex_top_iff

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.IsFiniteRelIndex ⊤
⊢ H.IsFiniteRelIndex K
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
h : H < K
inst✝ : H.FiniteIndex
h0 : K.index ≠ 0
⊢ K.index < H.index

Tactic:
apply lt_of_le_of_ne (index_antitone h.le)

Goal state after:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
h : H < K
inst✝ : H.FiniteIndex
h0 : K.index ≠ 0
⊢ K.index ≠ H.index
Module: Mathlib.Algebra.Algebra.ZMod

Goal state before:
pp: R✝ : Type u_1
inst✝⁴ : Ring R✝
n : ℕ
R : Type u_2
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module (ZMod n) R
m₁ : Module (ZMod n) M
inst✝ : Module R M
this : Algebra (ZMod n) R := algebraOfModule n R
m₂ : Module (ZMod n) M := Module.compHom M (algebraMap (ZMod n) R)
⊢ IsScalarTower (ZMod n) R M

Tactic:
obtain rfl : m₁ = m₂ := Subsingleton.elim _ _

Goal state after:
R✝ : Type u_1
inst✝⁴ : Ring R✝
n : ℕ
R : Type u_2
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module (ZMod n) R
inst✝ : Module R M
this : Algebra (ZMod n) R := algebraOfModule n R
m₂ : Module (ZMod n) M := Module.compHom M (algebraMap (ZMod n) R)
⊢ IsScalarTower (ZMod n) R M
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a b : ZMod (n✝ + 1)
⊢ (a + b).val = (a.val + b.val) % (n✝ + 1)

Tactic:
apply Fin.val_add

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ (a + b).val = a.val + b.val - n

Tactic:
rw [val_add_val_of_le h]

Goal state after:
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ (a + b).val = (a + b).val + n - n
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
this : Std.Asymm fun x1 x2 ↦ x1.2 < x2.2
⊢ n.divisorsAntidiagonalList.reverse.Perm (List.map Prod.swap n.divisorsAntidiagonalList)

Tactic:
simp [List.reverse_perm', List.perm_ext_iff_of_nodup nodup_divisorsAntidiagonalList
    (nodup_divisorsAntidiagonalList.map Prod.swap_injective), mul_comm]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.properDivisors = ∅ ↔ n ≤ 1

Tactic:
by
  contrapose!
  exact nonempty_properDivisors

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a * b / (b - 1) = (a * 1 + a * (b - 1)) / (b - 1)

Tactic:
rw [← mul_add, add_tsub_cancel_of_le (by lia)]

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

Goal state before:
pp: case mp.zero
⊢ Subsingleton (ZMod 0) → 0 = 1

Tactic:
simpa [ZMod] using not_subsingleton _

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

Goal state before:
pp: case mp.succ.succ
n : ℕ
⊢ Subsingleton (ZMod (n + 1 + 1)) → n + 1 + 1 = 1

Tactic:
simpa [ZMod] using not_subsingleton _

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

Goal state before:
pp: a : ℤ
⊢ ↑|a| = ↑a

Tactic:
by
  cases le_total a 0 <;> simp [abs_of_nonneg, abs_of_nonpos, *]

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

Goal state before:
pp: n b : ℕ
hb : 2 ≤ b
hn : 0 < n
⊢ b.digits n = n % b :: b.digits (n / b)

Tactic:
by
  rw [Nat.eq_add_of_sub_eq hb rfl, Nat.eq_add_of_sub_eq hn rfl, Nat.digits_add_two_add_one]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

Tactic:
rw [hb.multiplicity_add_of_gt hab, min_eq_right]

Goal state after:
case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p b ≤ multiplicity p a
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x

Tactic:
obtain ⟨m, -, h⟩ := exists_mul_mod_eq_one_of_coprime h (by lia)

Goal state after:
case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h✝ : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
have hdiva : p ^ multiplicity p a ∣ a := pow_multiplicity_dvd ..
  have hdivb : p ^ multiplicity p b ∣ b := pow_multiplicity_dvd ..
  have hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b := by
    rw [pow_add]; gcongr
  have hsucc : ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b :=
    fun h =>
    not_or_intro (hfin.mul_left.not_pow_dvd_of_multiplicity_lt (lt_succ_self _))
      (hfin.mul_right.not_pow_dvd_of_multiplicity_lt (lt_succ_self _))
      (_root_.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul hp hdiva hdivb h)
  rw [hfin.multiplicity_eq_iff]
  exact ⟨hdiv, hsucc⟩

Goal state after:
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:
ENat.add_eq_top,

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.Data.Nat.Factorization.Basic

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

Tactic:
by_cases pp : p.Prime

Goal state after:
case pos
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ n.factorization p < n

case neg
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ n.factorization p < n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n p : ℕ
hp : Fact (Nat.Prime p)
hnot : ¬x ^ p ^ n = 1
hfin : x ^ p ^ (n + 1) = 1
⊢ orderOf x = p ^ (n + 1)

Tactic:
by
  apply minimalPeriod_eq_prime_pow <;> rwa [isPeriodicPt_mul_iff_pow_eq_one]

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

Goal state before:
pp: case hf
n k : ℕ
hkn : k ≤ n
p : ℕ
a✝ : p ∈ Finset.range (n + 1)
⊢ p ∉ (n.choose k).factorization.support → (fun x1 x2 ↦ x1 ^ x2) p ((n.choose k).factorization p) = 1

Tactic:
h2

Goal state after:
case hf
n k : ℕ
hkn : k ≤ n
p : ℕ
a✝ : p ∈ Finset.range (n + 1)
h2 : p ∉ (n.choose k).factorization.support
⊢ (fun x1 x2 ↦ x1 ^ x2) p ((n.choose k).factorization p) = 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hda
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ((a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2) ∣ a

Tactic:
exact prod_pow_dvd_of_le_factorization inf_le_left

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x y : G
h : orderOf x = orderOf y
n : ℕ
⊢ (finEquivPowers ⋯) ((finCongr h) ⟨n % orderOf x, ⋯⟩) = ⟨y ^ n, ⋯⟩

Tactic:
←
    Equiv.eq_symm_apply,

Goal state after:
G : Type u_1
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x y : G
h : orderOf x = orderOf y
n : ℕ
⊢ (finCongr h) ⟨n % orderOf x, ⋯⟩ = (finEquivPowers ⋯).symm ⟨y ^ n, ⋯⟩
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ n = n - k + k

pp: p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ log p (n - k + k) < b

Tactic:
· rw [this]

Goal state after:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ log p (n - k + k) < b
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
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : ExpChar S p
x : R
n : ℕ
⊢ f ((iterateFrobenius R p n) x) = (iterateFrobenius S p n) (f x)

Tactic:
by
  simp [iterateFrobenius_def]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
x y : G
inst✝ : Finite G
h : orderOf x = orderOf y
n : ℕ
⊢ (finEquivZPowers ⋯) ((finCongr h) ⟨n % orderOf x, ⋯⟩) = ⟨y ^ n, ⋯⟩

Tactic:
←
    Equiv.eq_symm_apply,

Goal state after:
G : Type u_1
inst✝¹ : Group G
x y : G
inst✝ : Finite G
h : orderOf x = orderOf y
n : ℕ
⊢ (finCongr h) ⟨n % orderOf x, ⋯⟩ = (finEquivZPowers ⋯).symm ⟨y ^ n, ⋯⟩
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
⊢ a.factorization p = b.factorization p

Tactic:
by_cases pp : p.Prime

Goal state after:
case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : Prime p
⊢ a.factorization p = b.factorization p

case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : ¬Prime p
⊢ a.factorization p = b.factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b ↔ ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b

Tactic:
by
  constructor
  · rintro rfl
    simp
  · intro h
    refine eq_of_factorization_eq ha hb fun p => ?_
    by_cases pp : p.Prime
    · simp [factorization_def, pp, h p pp]
    · simp [factorization_eq_zero_of_not_prime, pp]

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

Goal state before:
pp: case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
⊢ (C c * (X ^ n).divX).natDegree = n - 1

Tactic:
divX_X_pow

Goal state after:
case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
⊢ (C c * if n = 0 then 0 else X ^ (n - 1)).natDegree = n - 1
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
Nat.cast_card_eq_zero

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 : ℕ
⊢ 0 = 0
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
⊢ ↑n = 0 → p ∣ n

Tactic:
intro h
      rw [← Nat.mod_add_div n p, Nat.cast_add, Nat.cast_mul, H, zero_mul, add_zero] at h
      rw [Nat.dvd_iff_mod_eq_zero]
      apply hR _ (Nat.mod_lt _ _) h
      rw [← hn, Fintype.card_pos_iff]
      exact ⟨0⟩

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
⊢ ↑(card R) = 0

Tactic:
Nat.cast_card_eq_zero

Goal state after:
R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
r : R
⊢ (expand R p) ((monomial q) r) = (monomial (q * p)) r

Tactic:
by
  simp_rw [← smul_X_eq_monomial, map_smul, map_pow, expand_X, mul_comm, pow_mul]

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.coeff (n / p) = 0

Tactic:
rw [coeff_eq_zero_of_natDegree_lt]

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 : ℕ
hn : ↑(f.natDegree * p) < ↑n
hpn : p ∣ n
⊢ f.natDegree < n / p
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ p q : R[X]
⊢ ((p + q).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) =
    (p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) + q.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)

Tactic:
sum_add_index

Goal state after:
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ p q : R[X]
⊢ ((p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) + q.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) =
    (p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) + q.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)

case hf
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ p q : R[X]
⊢ ∀ (i : ℕ), C (0 * ↑i) * X ^ (i - 1) = 0

case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ p q : R[X]
⊢ ∀ (a : ℕ) (b₁ b₂ : R), C ((b₁ + b₂) * ↑a) * X ^ (a - 1) = C (b₁ * ↑a) * X ^ (a - 1) + C (b₂ * ↑a) * X ^ (a - 1)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
r : R
⊢ contract p (C r) = C r

Tactic:
simp [contract]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ ((x, y).1 + (x, y).2) * p = n * p

Tactic:
rw [← eq, mul_comm, mul_add]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
p : R[X]
h : Function.Injective ⇑(algebraMap A B)
⊢ (aeval ((algebraMap A B) x)) p = 0 ↔ (aeval x) p = 0

Tactic:
by
  rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
⊢ q ∣ q * p

Tactic:
exact dvd_mul_right q p

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : ¬p = 0
⊢ (X - C a) ^ rootMultiplicity a p ∣ p

Tactic:
rw [rootMultiplicity_eq_multiplicity, if_neg h]; apply pow_multiplicity_dvd

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

Goal state before:
pp: case mp
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ (∃ I,
      I.Finite ∧
        ∃ V, (∀ (i : ι), ∃ i_1, p i i_1 ∧ s i i_1 ⊆ V i) ∧ (∀ i ∉ I, V i = univ) ∧ t = ⋂ i ∈ I, V i ∧ t = ⋂ i, V i) →
    ∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t

Tactic:
rintro ⟨I, hI, V, hV, -, rfl, -⟩

Goal state after:
case mp
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
I : Set ι
hI : I.Finite
V : ι → Set α
hV : ∀ (i : ι), ∃ i_1, p i i_1 ∧ s i i_1 ⊆ V i
⊢ ∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ ⋂ i ∈ I, V i
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)
⊢ (⨅ x, f x.down).IsCountablyGenerated

Tactic:
refine HasCountableBasis.isCountablyGenerated ⟨.iInf fun n => (hs _).1, ?_⟩

Goal state after:
α✝ : 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)
⊢ {If | If.fst.Finite ∧ ∀ (i : ↑If.fst), True}.Countable
Module: Mathlib.Order.Filter.Ker

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
f✝ g : Filter α
s✝ : Set α
a : α
s : Set α
f : Filter α
⊢ 𝓟 s ≤ f ↔ s ⊆ f.ker

Tactic:
by simp [principal_le_iff]

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

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

Tactic:
exact dif_neg hi

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

Goal state before:
pp: α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ U ∈ ⨅ i, s i ↔ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ i ∈ I, V i ∧ U = ⋂ i, V i

Tactic:
simp only [mem_iInf, biInter_eq_iInter]
  refine ⟨?_, fun ⟨I, If, V, hVs, _, hVU, _⟩ => ⟨I, If, fun i => V i, fun i => hVs i, hVU⟩⟩
  rintro ⟨I, If, V, hV, rfl⟩
  refine ⟨I, If, fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ, fun i => ?_, fun i hi => ?_, ?_⟩
  · dsimp only
    split_ifs
    exacts [hV ⟨i,_⟩, univ_mem]
  · exact dif_neg hi
  · 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: case inr
R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
k : ℕ
hk : k ∈ range n.succ
hk' : k ∉ range (min m n).succ
hkm : m < k
⊢ (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k)) = 0

Tactic:
· simp [Nat.descFactorial_eq_zero_iff_lt.mpr hkm]

Goal state after: