mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case refine_4
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
x : R ⧸ I ^ (n + 1)
hx : x ∈ map (Quotient.mk (I ^ (n + 1))) (I ^ n)
⊢ ∃ a, (fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩) a = ⟨x, hx⟩

Tactic:
rw [Ideal.mem_map_iff_of_surjective _ Ideal.Quotient.mk_surjective] at hx

Goal state after:
case refine_4
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
x : R ⧸ I ^ (n + 1)
hx✝ : x ∈ map (Quotient.mk (I ^ (n + 1))) (I ^ n)
hx : ∃ x_1 ∈ I ^ n, (Quotient.mk (I ^ (n + 1))) x_1 = x
⊢ ∃ a, (fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩) a = ⟨x, hx✝⟩
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m : ℕ
hm : m ∈ List.range (minimalPeriod f x)
n : ℕ
hn : n ∈ List.range (minimalPeriod f x)
⊢ f^[m] x = f^[n] x → m = n

Tactic:
hmn

Goal state after:
α : Type u_1
f : α → α
x : α
m : ℕ
hm : m ∈ List.range (minimalPeriod f x)
n : ℕ
hn : n ∈ List.range (minimalPeriod f x)
hmn : f^[m] x = f^[n] x
⊢ m = n
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
h : xs.nextOr x d ≠ d
⊢ x ∈ xs

Tactic:
by
  induction xs with
  | nil => simp at h
  | cons y ys IH => ?_
  rcases ys with - | ⟨z, zs⟩
  · simp at h
  · by_cases hx : x = y
    · simp [hx]
    · rw [nextOr_cons_of_ne _ _ _ _ hx] at h
      simpa [hx] using IH h

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

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℕ
⊢ a ^ n • b = b ↔ minimalPeriod (fun x ↦ a • x) b ∣ n

Tactic:
rw [← period_eq_minimalPeriod, pow_smul_eq_iff_period_dvd]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x✝ : α
h : x✝ ∈ []
⊢ α

Tactic:
by simp at h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
⊢ List.beq = fun a b ↦ decide (a = b)

Tactic:
funext l₁ l₂
    change (l₁ == l₂) = _
    rw [Bool.eq_iff_iff, @beq_iff_eq _ (_), decide_eq_true_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l ≠ []
h : l.getLast hl ∉ l.dropLast
d : α
⊢ l.nextOr (l.getLast hl) d = d

Tactic:
by
  match l with
  | nil | [_] => simp
  | x :: y :: tail =>
    unfold nextOr
    split_ifs with h'
    · grind
    apply nextOr_getLast_of_notMem_dropLast
    grind

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

Goal state before:
pp: G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
hH : H.Normal
x✝³ : Gᵐᵒᵖ
x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ (unop x✝³)⁻¹ * (x✝²⁻¹ * (x✝¹ * unop x✝³)) ∈ H

Tactic:
hH.mem_comm_iff,

Goal state after:
G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
hH : H.Normal
x✝³ : Gᵐᵒᵖ
x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ x✝²⁻¹ * (x✝¹ * unop x✝³) * (unop x✝³)⁻¹ ∈ H
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:
by
  rw [sup_comm, relIndex_sup_right]

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

Goal state before:
pp: a b : ℕ
h : a = b
x : ZMod a
⊢ ((ringEquivCongr h) x).val = x.val

Tactic:
subst h
  cases a <;> rfl

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

Goal state before:
pp: p n : ℕ
h : 0 ≤ Int.negSucc n
⊢ ↑(Int.negSucc n).toNat = ↑(Int.negSucc n)

Tactic:
by simp at h

Goal state after:
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
inst✝ : Module R M
this : Algebra (ZMod n) R := algebraOfModule n R
m₂ : Module (ZMod n) M := Module.compHom M (algebraMap (ZMod n) R)
x : ZMod n
y : R
z : M
⊢ (x • y) • z = x • y • z

Tactic:
Algebra.smul_def,

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)
x : ZMod n
y : R
z : M
⊢ ((algebraMap (ZMod n) R) x * y) • z = x • y • z
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
⊢ IsScalarTower (ZMod n) R M

Tactic:
let := ZMod.algebraOfModule n R
  let m₂ := Module.compHom M (algebraMap (ZMod n) R)
  obtain rfl : m₁ = m₂ := Subsingleton.elim _ _
  exact ⟨fun x y z ↦ by rw [Algebra.smul_def, mul_smul]; rfl⟩

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ List.Pairwise (fun x1 x2 ↦ x1.2 > x2.2) n.divisorsAntidiagonalList

Tactic:
obtain rfl | hn := eq_or_ne n 0
  · simp
  refine (List.sortedLT_range' _ _ Nat.one_ne_zero).pairwise.filterMap _ ?_
  simp only [Option.ite_none_right_eq_some, Option.some.injEq, gt_iff_lt,
    and_imp, Prod.forall, Prod.mk.injEq]
  rintro a b hab _ _ ha rfl rfl _ _ hb rfl rfl
  rwa [Nat.div_lt_div_left hn ⟨_, hb.symm⟩ ⟨_, ha.symm⟩]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ image (Prod.snd ∘ ⇑(Equiv.prodComm ℕ ℕ).toEmbedding) n.divisorsAntidiagonal = n.divisors

Tactic:
exact image_fst_divisorsAntidiagonal

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

Goal state before:
pp: n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
H : a * a⁻¹ * b = a * 1
⊢ a = b

Tactic:
a.mul_inv_of_unit ha,

Goal state after:
n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
H : 1 * b = a * 1
⊢ a = b
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ
⊢ 1 = ∑ x ∈ (n + 1 + 1).properDivisors, x

Tactic:
← mem_singleton,

Goal state after:
case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ
⊢ 1 ∈ {∑ x ∈ (n + 1 + 1).properDivisors, x}
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.mp.succ.succ
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ 2 * (n✝¹ + 1) ≤ 2 * a.val

Tactic:
he,

Goal state after:
case succ.mp.succ.succ
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ 2 * (n✝¹ + 1) ≤ (n✝¹ + 1) * (n✝ + 1 + 1)
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: ⊢ ∀ (n : ℕ), n.centralBinom < (n + 1).centralBinom

Tactic:
grind [Nat.choose_pos, centralBinom]

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

Goal state before:
pp: b : ℕ
l : List ℕ
d : ℕ
⊢ ofDigits b (d :: l).reverse = ofDigits b l.reverse + b ^ l.length * d

Tactic:
simp only [List.reverse_cons]
  rw [ofDigits_append]
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
b : ℕ
L : List ℕ
⊢ ↑(ofDigits b L) = ofDigits (↑b) L

Tactic:
by
  induction L with
  | nil => simp [ofDigits]
  | cons d L ih => dsimp [ofDigits]; push_cast; rw [ih]

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

Goal state before:
pp: case cons
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : ∀ (h : d :: L ≠ []), (d :: L).getLast h ≠ 0
⊢ b.digits (ofDigits b (d :: L)) = d :: L

Tactic:
dsimp [ofDigits]
    replace w₂ := w₂ (by simp)
    rw [digits_add b h]
    · rw [ih]
      · intro l m
        apply w₁
        exact List.mem_cons_of_mem _ m
      · intro h
        rw [List.getLast_cons h] at w₂
        convert! w₂
    · exact w₁ d List.mem_cons_self
    · by_cases h' : L = []
      · rcases h' with rfl
        left
        simpa using w₂
      · right
        contrapose w₂
        refine digits_zero_of_eq_zero h.ne_bot w₂ _ ?_
        rw [List.getLast_cons h']
        exact List.getLast_mem h'

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

Goal state before:
pp: case cons
n b hd : ℕ
tl : List ℕ
ih : n * ofDigits b tl = ofDigits b (List.map (fun x ↦ n * x) tl)
⊢ n * ofDigits b (hd :: tl) = ofDigits b (List.map (fun x ↦ n * x) (hd :: tl))

Tactic:
rw [List.map_cons, ofDigits_cons, ofDigits_cons, ← ih]

Goal state after:
case cons
n b hd : ℕ
tl : List ℕ
ih : n * ofDigits b tl = ofDigits b (List.map (fun x ↦ n * x) tl)
⊢ n * (hd + b * ofDigits b tl) = n * hd + b * (n * ofDigits b tl)
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p k n : ℕ
hp : p ≠ 1
hn : n ≠ 0
⊢ p ^ k ∣ n ↔ k ≤ padicValNat p n

Tactic:
obtain rfl | hp₁ : p = 0 ∨ 1 < p := by grind

Goal state after:
case inl
k n : ℕ
hn : n ≠ 0
hp : 0 ≠ 1
⊢ 0 ^ k ∣ n ↔ k ≤ padicValNat 0 n

case inr
p k n : ℕ
hp : p ≠ 1
hn : n ≠ 0
hp₁ : 1 < p
⊢ p ^ k ∣ n ↔ k ≤ padicValNat p n
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inr.inl
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < 1
⊢ (1 - 1) * ∑ i ∈ range L.length, ofDigits 1 L / 1 ^ i.succ = ofDigits 1 L - L.sum

Tactic:
simp [ofDigits_one]

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

Goal state before:
pp: case succ.cons
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ (hd + p * ofDigits p tl % (p * p ^ i)) % (p * p ^ i) = hd + p * (ofDigits p tl % p ^ i)

Tactic:
mul_mod_mul_left,

Goal state after:
case succ.cons
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ (hd + p * (ofDigits p tl % p ^ i)) % (p * p ^ i) = hd + p * (ofDigits p tl % p ^ i)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝ : DivisionMonoid G
x : G
⊢ IsOfFinOrder x ↔ ∃ n, n ≠ 0 ∧ x ^ n = 1

Tactic:
by
  rw [isOfFinOrder_iff_pow_eq_one]
  refine ⟨fun ⟨n, hn, hn'⟩ ↦ ⟨n, Int.natCast_ne_zero_iff_pos.mpr hn, zpow_natCast x n ▸ hn'⟩,
    fun ⟨n, hn, hn'⟩ ↦ ⟨n.natAbs, Int.natAbs_pos.mpr hn, ?_⟩⟩
  rcases (Int.natAbs_eq_iff (a := n)).mp rfl with h | h
  · rwa [h, zpow_natCast] at hn'
  · rwa [h, zpow_neg, inv_eq_one, zpow_natCast] at hn'

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: p : ℕ
hp : p ≠ 1
n : ℕ
hn : n ≠ 0
⊢ ↑(padicValNat p n) = emultiplicity p n

Tactic:
rw [eq_comm, emultiplicity_eq_coe, pow_dvd_iff_le_padicValNat hp hn,
    pow_dvd_iff_le_padicValNat hp hn]
  simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : IsConj x y
n : ℕ
n_gt_0 : 0 < n
eq' : x ^ n = 1
⊢ IsConj 1 (y ^ n)

Tactic:
← eq'

Goal state after:
G : Type u_1
inst✝ : Monoid G
x y : G
h : IsConj x y
n : ℕ
n_gt_0 : 0 < n
eq' : x ^ n = 1
⊢ IsConj (x ^ n) (y ^ n)
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ p ∈ f.support, Prime p
⊢ f = n.factorization ↔ (f.prod fun x1 x2 ↦ x1 ^ x2) = n

Tactic:
constructor <;> rintro rfl
  exacts [prod_factorization_pow_eq_self hn, prod_pow_factorization_eq_self hf |>.symm]

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}) + (k ! * n !).factorization p

Tactic:
factorization_mul (factorial_ne_zero k) (factorial_ne_zero 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, (n + k) / p ^ i =
    #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}) + (k !.factorization + n !.factorization) p
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
⊢ (n.choose k).factorization p ≤ log p n

Tactic:
have hkn : k ≤ n := by
    refine le_of_not_gt fun hnk => h ?_
    simp [choose_eq_zero_of_lt hnk]

Goal state after:
case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
hkn : k ≤ n
⊢ (n.choose k).factorization p ≤ log p n
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 : ℕ
⊢ ∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k) =
    x ^ p ^ n + y ^ p ^ n + ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k)

Tactic:
Icc_eq_cons_Ico zero_le,

Goal state after:
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) (Ico 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)
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p ((p ^ n).choose k) + emultiplicity p k ≤ ↑n

Tactic:
have hdisj :
        Disjoint {i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}
          {i ∈ Ico 1 n.succ | p ^ i ∣ k} := by
        simp +contextual [disjoint_right, *, dvd_iff_mod_eq_zero,
          Nat.mod_lt _ (pow_pos hp.pos _)]

Goal state after:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ emultiplicity p ((p ^ n).choose k) + emultiplicity p k ≤ ↑n
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
⊢ (_root_.frobenius S p) (r • s) = (_root_.frobenius R p) r • (↑↑(_root_.frobenius S p)).toFun s

Tactic:
Algebra.smul_def,

Goal state after:
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
⊢ (_root_.frobenius S p) ((algebraMap R S) r * s) =
    (algebraMap R S) ((_root_.frobenius R p) r) * (↑↑(_root_.frobenius S p)).toFun s
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
⊢ (f • s) ^ p ^ n = f ^ p ^ n • (↑↑(_root_.iterateFrobenius S p n)).toFun s

Tactic:
Algebra.smul_def,

Goal state after:
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 * s) ^ p ^ n = (algebraMap R S) (f ^ p ^ n) * (↑↑(_root_.iterateFrobenius S p n)).toFun s
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n k : ℕ
hp : Prime p
⊢ p ∣ (p ^ n).choose k ↔ k ≠ 0 ∧ k ≠ p ^ n

Tactic:
refine ⟨fun h => ⟨?_, ?_⟩, fun h => dvd_choose_pow hp h.1 h.2⟩ <;> rintro rfl <;>
    simp [hp.ne_one] at h

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
k : ℕ
k_pos : k ≠ 0
ha : a ^ k = 1
⊢ orderOf a ≤ k

Tactic:
apply orderOf_le_of_pow_eq_one k_pos.bot_lt ha

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ c • (p %ₘ q + q * (p /ₘ q)) = c • p

Tactic:
modByMonic_add_div

Goal state after:
R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ c • p = c • 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✝ : R[X]
a : R
p : R[X]
⊢ ((a • p).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) = (RingHom.id R) a • p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)

Tactic:
dsimp; rw [sum_smul_index] <;>
      simp only [mul_sum, ← C_mul', mul_assoc, map_mul, forall_const, zero_mul, map_zero, sum]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (∑ n_1 ∈ p.support, p.coeff n_1 * ↑n_1 * if n = n_1 - 1 then 1 else 0) = p.coeff (n + 1) * (↑n + 1)

Tactic:
Finset.sum_eq_single (n + 1)

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.coeff (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = p.coeff (n + 1) * (↑n + 1)

case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ∀ b ∈ p.support, b ≠ n + 1 → (p.coeff b * ↑b * if n = b - 1 then 1 else 0) = 0

case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ n + 1 ∉ p.support → (p.coeff (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq R
x y : R
⊢ rootMultiplicity x (X - C y) = if x = y then 1 else 0

Tactic:
split_ifs with hxy
  · rw [hxy]
    exact rootMultiplicity_X_sub_C_self
  exact rootMultiplicity_eq_zero (mt root_X_sub_C.mp (Ne.symm hxy))

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ X ∣ p - C (p.coeff 0)

Tactic:
by
  simp [X_dvd_iff, coeff_C]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (if p * q = 0 then 0 else multiplicity (X - C x) (p * q)) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
if_neg hpq,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ multiplicity (X - C x) (p * q) = rootMultiplicity x p + rootMultiplicity x q
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q

Tactic:
nontriviality S

Goal state after:
R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
a✝ : Nontrivial S
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
a✝ : Nontrivial S
this : Nontrivial R
⊢ map f p = map f (p %ₘ q + q * (p /ₘ q))

Tactic:
modByMonic_add_div

Goal state after:
R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
a✝ : Nontrivial S
this : Nontrivial R
⊢ map f p = map f p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ p₁ %ₘ q + q * (p₁ /ₘ q) + p₂ = p₁ + p₂

Tactic:
modByMonic_add_div

Goal state after:
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ p₁ + p₂ = p₁ + p₂
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
⊢ (⨅ i, f i).sets = ⋃ t, (⨅ i ∈ t, f i.down).sets

Tactic:
by
  rw [← iInf_sets_eq_finite, ← Equiv.plift.surjective.iInf_comp, Equiv.plift_apply]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f₁ i).NeBot
⊢ pi f₁ = pi f₂ ↔ f₁ = f₂

Tactic:
by
  refine ⟨fun h => ?_, congr_arg pi⟩
  have hle : f₁ ≤ f₂ := pi_le_pi.1 h.le
  have : ∀ i, NeBot (f₂ i) := fun i => neBot_of_le (hle i)
  exact hle.antisymm (pi_le_pi.1 h.ge)

Goal state after:
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₂ : p.leadingCoeff = q.leadingCoeff
⊢ p = q

Tactic:
rcases eq_or_ne q 0 with rfl | hq
  · simpa using h₂
  replace h₁ := (natDegree_le_of_dvd hpq hq).antisymm h₁
  obtain ⟨u, rfl⟩ := hpq
  rw [mul_ne_zero_iff] at hq
  rw [natDegree_mul hq.1 hq.2, left_eq_add] at h₁
  rw [eq_C_of_natDegree_eq_zero h₁, leadingCoeff_mul, leadingCoeff_C,
    eq_comm, mul_eq_left₀ (leadingCoeff_ne_zero.mpr hq.1)] at h₂
  rw [eq_C_of_natDegree_eq_zero h₁, h₂, map_one, mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
⊢ (a ∧ b ∨ ¬(a ∧ b)) ∧ ((a ∨ b) ∨ ¬(a ∨ b)) → a ∨ ¬a

Tactic:
by
  rintro ⟨⟨ha, _⟩ | hnab, (ha | hb) | hnab⟩ <;> try exact Or.inl ha
  · exact Or.inr fun ha => hnab ⟨ha, hb⟩
  · exact Or.inr fun ha => hnab <| Or.inl ha

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

Goal state before:
pp: M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : Subsingleton M₀ˣ
s : Finset M₀
n : M₀
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
⊢ ∀ a ∈ Multiset.map (fun p ↦ p) s.val, Prime a

Tactic:
simpa only [Multiset.map_id', Finset.mem_def] using h

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

Goal state before:
pp: case mpr
σ : Type u_1
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
⊢ f = 0 → (weight w) f = 0

Tactic:
intro h
    rw [h, map_zero]

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 normalize (normalizedFactors (x * y)) =
    Multiset.map (fun x ↦ x) (normalizedFactors x) + Multiset.map (fun x ↦ x) (normalizedFactors y)

Tactic:
←
    Multiset.map_congr rfl normalize_normalized_factor,

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 normalize (normalizedFactors (x * y)) =
    Multiset.map normalize (normalizedFactors x) + Multiset.map (fun x ↦ x) (normalizedFactors y)
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 normalize (normalizedFactors (x * y)) =
    Multiset.map normalize (normalizedFactors x) + Multiset.map (fun x ↦ x) (normalizedFactors y)

Tactic:
←
    Multiset.map_congr rfl normalize_normalized_factor,

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 normalize (normalizedFactors (x * y)) =
    Multiset.map normalize (normalizedFactors x) + Multiset.map normalize (normalizedFactors y)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p x : α
h : x ≠ 0
x✝ : Irreducible p ∧ normalize p = p ∧ p ∣ x
h₁ : Irreducible p
h₂ : normalize p = p
h₃ : p ∣ x
y : α
hy₁ : y ∈ factors x
hy₂ : p ~ᵤ y
⊢ normalize y = normalize p

Tactic:
normalize_eq_normalize_iff_associated,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p x : α
h : x ≠ 0
x✝ : Irreducible p ∧ normalize p = p ∧ p ∣ x
h₁ : Irreducible p
h₂ : normalize p = p
h₃ : p ∣ x
y : α
hy₁ : y ∈ factors x
hy₂ : p ~ᵤ y
⊢ y ~ᵤ p