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

Goal state before:
pp: n k a : ℕ
⊢ (∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p) → List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: (k + 2).primeFactorsList)

Tactic:
h

Goal state after:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
⊢ List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: (k + 2).primeFactorsList)
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: (k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList)

Tactic:
refine List.IsChain.cons_cons
        ((le_minFac.2 h).resolve_left (by simp)) (isChain_cons_primeFactorsList ?_)

Goal state after:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ ∀ (p : ℕ), Prime p → p ∣ (k + 2) / (k + 2).minFac → (k + 2).minFac ≤ p
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case mp.succ.zero
h : (0 + 1).primeFactorsList = []
⊢ 0 + 1 = 0 ∨ 0 + 1 = 1

pp: case mp.succ.succ
n : ℕ
h : (n + 1 + 1).primeFactorsList = []
⊢ n + 1 + 1 = 0 ∨ n + 1 + 1 = 1

Tactic:
· exact Or.inr rfl

Goal state after:
case mp.succ.succ
n : ℕ
h : (n + 1 + 1).primeFactorsList = []
⊢ n + 1 + 1 = 0 ∨ n + 1 + 1 = 1
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : orbitRel.Quotient (↥H) X
y₁ y₂ : X
⊢ (orbitRel (↥H) X) y₁ y₂ → ↑⋯.choose = ↑⋯.choose

Tactic:
h

Goal state after:
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : orbitRel.Quotient (↥H) X
y₁ y₂ : X
h : (orbitRel (↥H) X) y₁ y₂
⊢ ↑⋯.choose = ↑⋯.choose
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : G ⧸ H
g₁ g₂ : G
⊢ (leftRel H) g₁ g₂ → ⟦g₁⁻¹ • x⟧ = ⟦g₂⁻¹ • x⟧

Tactic:
h

Goal state after:
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : G ⧸ H
g₁ g₂ : G
h : (leftRel H) g₁ g₂
⊢ ⟦g₁⁻¹ • x⟧ = ⟦g₂⁻¹ • x⟧
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case pos
n : ℕ
a b : Fin (n + 1)
h : n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b - (n + 1)) = cast a + cast b - ↑(n + 1)

Tactic:
rw [Nat.cast_sub h]
    congr

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Finite (G ⧸ H)
⊢ H.index ≠ 0

Tactic:
by
  cases nonempty_fintype (G ⧸ H)
  rw [index_eq_card]
  exact Nat.card_pos.ne'

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
this : NeZero n
⊢ Injective ⇑(castHom ⋯ R) ∧ Fintype.card (ZMod n) = Fintype.card R

Tactic:
ZMod.card,

Goal state after:
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
this : NeZero n
⊢ Injective ⇑(castHom ⋯ R) ∧ n = Fintype.card R
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
this : ∃ n₁ n₂, n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)

Tactic:
by
    rcases this with ⟨n₁, n₂, hne, hle₁, hle₂, he⟩
    rcases hne.lt_or_gt with hlt | hlt
    · exact ⟨n₁, n₂, hlt, hle₂, he⟩
    · exact ⟨n₂, n₁, hlt, hle₁, he.symm⟩

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

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

Tactic:
h

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

Goal state before:
pp: case mp
n : ℕ
h✝ : 0 < n
h : ∑ i ∈ n.properDivisors, i = n
⊢ ∑ i ∈ n.properDivisors, i + n = n + n

Tactic:
h

Goal state after:
case mp
n : ℕ
h✝ : 0 < n
h : ∑ i ∈ n.properDivisors, i = n
⊢ n + n = n + n
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ ¬∑ i ∈ range n, x ^ i < 0 ↔ ¬(Even n ∧ x + 1 < 0)

Tactic:
not_lt,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ 0 ≤ ∑ i ∈ range n, x ^ i ↔ ¬(Even n ∧ x + 1 < 0)
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → ¬x + 1 < 0

Tactic:
not_lt,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → 0 ≤ x + 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∈ ↑n.divisors
y : ℕ
hy : y ∈ ↑n.divisors
⊢ n / x = n / y → x = y

Tactic:
h

Goal state after:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∈ ↑n.divisors
y : ℕ
hy : y ∈ ↑n.divisors
h : n / x = n / y
⊢ x = y
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mpr
n : ℕ
⊢ n = 1 → Subsingleton (ZMod n)

Tactic:
· rintro rfl
    infer_instance

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

Goal state before:
pp: case succ.mpr.inr
n✝ : ℕ
a : ZMod (n✝ + 1)
h : 2 * a.val = n✝ + 1
⊢ n✝ + 1 ∣ 2 * a.val

Tactic:
h

Goal state after:
case succ.mpr.inr
n✝ : ℕ
a : ZMod (n✝ + 1)
h : 2 * a.val = n✝ + 1
⊢ n✝ + 1 ∣ n✝ + 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
hm : NeZero m
h : m ≤ n
a : ZMod m
⊢ a.cast.cast = a

Tactic:
have : NeZero n := ⟨((Nat.zero_lt_of_ne_zero hm.out).trans_le h).ne'⟩
  rw [cast_eq_val, val_cast_eq_val_of_lt (a.val_lt.trans_le h), natCast_zmod_val]

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

Goal state before:
pp: case mp
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ f ↑n = 0 → AddSubgroup.zmultiples ↑n ≤ f.ker

Tactic:
rintro hf _ ⟨x, rfl⟩

Goal state after:
case mp
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
hf : f ↑n = 0
x : ℤ
⊢ (fun x ↦ x • ↑n) x ∈ f.ker
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case case1
n p✝ p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
e q : ℕ
heq : go n (p * p) ⋯ = (e, q)
hqp : q % p = 0
ih : (go n (p * p) ⋯).snd * (p * p) ^ (go n (p * p) ⋯).fst = n ∧ ¬p * p ∣ (go n (p * p) ⋯).snd
⊢ (2 * e + 1, q / p).snd * p ^ (2 * e + 1, q / p).fst = n ∧ ¬p ∣ (2 * e + 1, q / p).snd

Tactic:
heq

Goal state after:
case case1
n p✝ p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
e q : ℕ
heq : go n (p * p) ⋯ = (e, q)
hqp : q % p = 0
ih : (e, q).snd * (p * p) ^ (e, q).fst = n ∧ ¬p * p ∣ (e, q).snd
⊢ (2 * e + 1, q / p).snd * p ^ (2 * e + 1, q / p).fst = n ∧ ¬p ∣ (2 * e + 1, q / p).snd
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b n : ℕ
h : b.digits n = []
⊢ ofDigits b (b.digits n) = ofDigits b []

Tactic:
h

Goal state after:
b n : ℕ
h : b.digits n = []
⊢ ofDigits b [] = ofDigits b []
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case case2
n p✝ p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
e q : ℕ
heq : go n (p * p) ⋯ = (e, q)
hqp : ¬q % p = 0
ih : (go n (p * p) ⋯).snd * (p * p) ^ (go n (p * p) ⋯).fst = n ∧ ¬p * p ∣ (go n (p * p) ⋯).snd
⊢ (2 * e, q).snd * p ^ (2 * e, q).fst = n ∧ ¬p ∣ (2 * e, q).snd

Tactic:
heq

Goal state after:
case case2
n p✝ p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
e q : ℕ
heq : go n (p * p) ⋯ = (e, q)
hqp : ¬q % p = 0
ih : (e, q).snd * (p * p) ^ (e, q).fst = n ∧ ¬p * p ∣ (e, q).snd
⊢ (2 * e, q).snd * p ^ (2 * e, q).fst = n ∧ ¬p ∣ (2 * e, q).snd
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ}, L.length = L2.length → (∀ l ∈ L, l < b) → (∀ l ∈ L2, l < b) → ofDigits b L = ofDigits b L2 → L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
w2 : ∀ l_1 ∈ d :: l, l_1 < b
h : D + b * ofDigits b L = d + b * ofDigits b l
len : L.length = l.length
⊢ (D + b * ofDigits b L) % b = (d + b * ofDigits b l) % b

Tactic:
h

Goal state after:
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ}, L.length = L2.length → (∀ l ∈ L, l < b) → (∀ l ∈ L2, l < b) → ofDigits b L = ofDigits b L2 → L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
w2 : ∀ l_1 ∈ d :: l, l_1 < b
h : D + b * ofDigits b L = d + b * ofDigits b l
len : L.length = l.length
⊢ (d + b * ofDigits b l) % b = (d + b * ofDigits b l) % b
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case ind.zero
b d : ℕ
IH : ∀ m < 0, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ (b + 2).digits 0
⊢ d < b + 2

Tactic:
rw [digits_zero] at hd
    cases hd

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
nh : emultiplicity a b = ⊤
⊢ False

Tactic:
h

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
nh : ↑n = ⊤
⊢ False
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
nh : ¬FiniteMultiplicity a b
⊢ False

Tactic:
rw [← emultiplicity_eq_top, h] at nh

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
nh : ↑n = ⊤
⊢ False
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : emultiplicity a b = emultiplicity c d
⊢ WithTop.untopD 1 (emultiplicity a b) = WithTop.untopD 1 (emultiplicity c d)

Tactic:
h

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : emultiplicity a b = emultiplicity c d
⊢ WithTop.untopD 1 (emultiplicity c d) = WithTop.untopD 1 (emultiplicity c d)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mp.right
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ emultiplicity a b < ↑(n + 1)

Tactic:
h

Goal state after:
case mp.right
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ ↑n < ↑(n + 1)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: n b : ℕ
hb : 1 < b
l : ℕ
hn : n < b ^ l
⊢ (b.digitsAppend l n).length = l

Tactic:
rw [digitsAppend, length_append, length_replicate, Nat.add_sub_cancel']
  rwa [digits_length_le_iff hb]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
⊢ (∀ (n : ℕ), a ^ n ∣ b) ↔ a = 1 ∨ ¬0 < b

Tactic:
not_lt,

Goal state after:
a b : ℕ
⊢ (∀ (n : ℕ), a ^ n ∣ b) ↔ a = 1 ∨ b ≤ 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : IsConj x y
⊢ IsOfFinOrder x → IsOfFinOrder y

Tactic:
simp_rw [isOfFinOrder_iff_pow_eq_one]
  rintro ⟨n, n_gt_0, eq'⟩
  exact ⟨n, n_gt_0, by rw [← isConj_one_right, ← eq']; exact h.pow n⟩

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a : ℕ
b : ℤ
h : b = ↑b.natAbs
| emultiplicity (↑a) b

Tactic:
h

Goal state after:
a : ℕ
b : ℤ
h : b = ↑b.natAbs
| emultiplicity ↑a ↑b.natAbs
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a : ℕ
b : ℤ
h : b = -↑b.natAbs
| emultiplicity (↑a) b

Tactic:
h

Goal state after:
a : ℕ
b : ℤ
h : b = -↑b.natAbs
| emultiplicity (↑a) (-↑b.natAbs)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a : ℕ
b : ℤ
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) b

Tactic:
by
  rcases Int.natAbs_eq b with h | h <;> conv_rhs => rw [h]
  · rw [Int.natCast_emultiplicity]
  · rw [emultiplicity_neg, Int.natCast_emultiplicity]

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

Goal state before:
pp: n p k : ℕ
hn : n ≠ 0
h : n.factorization = single p k
⊢ (n.factorization.prod fun x1 x2 ↦ x1 ^ x2) = p ^ k

Tactic:
h

Goal state after:
n p k : ℕ
hn : n ≠ 0
h : n.factorization = single p k
⊢ ((single p k).prod fun x1 x2 ↦ x1 ^ x2) = p ^ k
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: n p : ℕ
hp : 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
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), m.factorization p = 0
⊢ ∑ i ∈ Ico 1 (p * n + 1), i.factorization p + ∑ i ∈ Ico (p * n + 1) (p * (n + 1) + 1), i.factorization p =
    (p * n)!.factorization p + ((n + 1).factorization p + 1)

Tactic:
sum_Ico_succ_top h2,

Goal state after:
n p : ℕ
hp : 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
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), m.factorization p = 0
⊢ ∑ i ∈ Ico 1 (p * n + 1), i.factorization p +
      (∑ k ∈ Ico (p * n + 1) (p * (n + 1)), k.factorization p + (p * (n + 1)).factorization p) =
    (p * n)!.factorization p + ((n + 1).factorization p + 1)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case mp
n p : ℕ
hp : Prime p
⊢ n / p ^ n.factorization p = n → n = 0 ∨ ¬p ∣ n

Tactic:
intro h
    by_cases n_zero : n = 0
    · simp [n_zero]
    · right
      rw [← h]
      exact not_dvd_ordCompl hp n_zero

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

Goal state before:
pp: k p : ℕ
hp : Prime p
m : ℕ
⊢ p ^ k * m / p ^ k / p ^ (p ^ k * m / p ^ k).factorization p = p ^ k * m / p ^ (p ^ k * m).factorization p

Tactic:
rw [Nat.mul_div_cancel_left m (pow_pos hp.pos k), ← ordCompl_self_pow_mul m k hp]

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

Goal state before:
pp: m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
fin : FiniteMultiplicity m n
i : ℕ
hi : 1 ≤ i
⊢ i ≤ multiplicity m n → i < b

Tactic:
h

Goal state after:
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
fin : FiniteMultiplicity m n
i : ℕ
hi : 1 ≤ i
h : i ≤ multiplicity m n
⊢ i < b
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
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
h : ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x ≠ ⊤
⊢ ∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x = emultiplicity p (n + 1) + 1

Tactic:
sum_Ico_succ_top h2,

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
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
h : ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x ≠ ⊤
⊢ ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + emultiplicity p (p * (n + 1)) = emultiplicity p (n + 1) + 1
Module: Mathlib.Algebra.CharP.Frobenius

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

Tactic:
mul_pow,

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 ^ p ^ n * 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: case refine_2
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
⊢ bit b n ≠ 0 → emultiplicity 2 (bit b n)! < ↑(bit b n)

Tactic:
h

Goal state after:
case refine_2
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
⊢ emultiplicity 2 (bit b n)! < ↑(bit b n)
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
inst✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g ^ ↑((Nat.card G).gcd n) = (g ^ ↑(Nat.card G)) ^ (Nat.card G).gcdA n * g ^ (↑n * (Nat.card G).gcdB n)
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g

Tactic:
zpow_mul',

Goal state after:
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g ^ ↑((Nat.card G).gcd n) = (g ^ ↑(Nat.card G)) ^ (Nat.card G).gcdA n * (g ^ (Nat.card G).gcdB n) ^ ↑n
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g
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 ‹_› ‹_›

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
f g : R[X]
⊢ (f + g).coeff n = f.coeff n + g.coeff n
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:
by
  rw [C_mul_X_pow_eq_monomial, C_mul_X_pow_eq_monomial, derivative_monomial]

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

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ C ((frobenius R p) a) * X ^ (n * p) = (C a * X ^ n) ^ p

Tactic:
mul_pow,

Goal state after:
case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ C ((frobenius R p) a) * X ^ (n * p) = C a ^ p * (X ^ n) ^ p
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:
by
  induction k generalizing p with
  | zero => simp
  | succ k ih =>
    simp only [ih, Function.iterate_succ, Polynomial.derivative_map, Function.comp_apply]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k i : ℕ
x✝ : i ∈ ((⇑derivative)^[k] p).support
⊢ C (((⇑derivative)^[k] p).coeff i) * X ^ i = C ((i + k).descFactorial k • p.coeff (i + k)) * X ^ i

Tactic:
rw [coeff_iterate_derivative, Nat.descFactorial_eq_factorial_mul_choose]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : (p %ₘ (X - C a)).coeff 0 = eval a p
this✝ : (p %ₘ (X - C a)).degree < 1
this : (p %ₘ (X - C a)).degree ≤ 0
⊢ C ((p %ₘ (X - C a)).coeff 0) = C (eval a p)

Tactic:
h

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : (p %ₘ (X - C a)).coeff 0 = eval a p
this✝ : (p %ₘ (X - C a)).degree < 1
this : (p %ₘ (X - C a)).degree ≤ 0
⊢ C (eval a p) = C (eval a p)
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mp
α : Type u
s : Set (Set α)
U : Set α
h : U ∈ generate s
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U

Tactic:
induction h with

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

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ (∃ t ⊆ ⋃ i, (s i).sets, t.Finite ∧ ⋂₀ t ⊆ U) → ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Tactic:
rintro ⟨t, tsub, tfin, tinter⟩

Goal state after:
case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
t : Set (Set α)
tsub : t ⊆ ⋃ i, (s i).sets
tfin : t.Finite
tinter : ⋂₀ t ⊆ U
⊢ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ
R : Type u
inst✝ : CommSemiring R
q : R[X]
n m : ℕ
ih : ∀ {p : R[X]}, q ^ n ∣ p → q ^ (n - m) ∣ (⇑derivative)^[m] p
p : R[X]
dvd : q ^ n ∣ p
⊢ q ^ (n - (m + 1)) ∣ (⇑derivative)^[m + 1] p

Tactic:
Nat.sub_succ,

Goal state after:
case succ
R : Type u
inst✝ : CommSemiring R
q : R[X]
n m : ℕ
ih : ∀ {p : R[X]}, q ^ n ∣ p → q ^ (n - m) ∣ (⇑derivative)^[m] p
p : R[X]
dvd : q ^ n ∣ p
⊢ q ^ (n - m).pred ∣ (⇑derivative)^[m + 1] p
Module: Mathlib.Order.Filter.Finite

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

Tactic:
rintro ⟨I, Ifin, V, V_in, rfl⟩
    exact mem_iInf_of_iInter Ifin V_in Subset.rfl

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
⊢ (∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ s) →
    ∀ (i : ι), ∃ t₁ ∈ f i, eval i ⁻¹' t₁ ⊆ (fun k i ↦ m i (k i)) ⁻¹' s

Tactic:
h

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
h : ∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ s
⊢ ∀ (i : ι), ∃ t₁ ∈ f i, eval i ⁻¹' t₁ ⊆ (fun k i ↦ m i (k i)) ⁻¹' s
Module: Mathlib.Order.Heyting.Boundary

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

Tactic:
exact Or.inr fun ha => hnab <| Or.inl ha

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
y : α → β
r : α → β → Prop
hy : Tendsto y f g
hr✝ : ∀ᶠ (p : α × β) in f ×ˢ g, r p.1 p.2
p : α → Prop
hp : ∀ᶠ (x : α) in f, p x
q : β → Prop
hq : ∀ᶠ (y : β) in g, q y
hr : ∀ {x : α}, p x → ∀ {y : β}, q y → r (x, y).1 (x, y).2
⊢ ∀ᶠ (x : α) in f, r x (y x)

Tactic:
filter_upwards [hp, hy.eventually hq] with _ hp hq using hr hp hq

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n k : ℕ
c : R
⊢ (⇑derivative)^[k] ((X + C (-c)) ^ n) = n.descFactorial k • (X + C (-c)) ^ (n - k)

Tactic:
iterate_derivative_X_add_pow

Goal state after:
R : Type u
inst✝ : CommRing R
n k : ℕ
c : R
⊢ n.descFactorial k • (X + C (-c)) ^ (n - k) = n.descFactorial k • (X + C (-c)) ^ (n - k)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case empty
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
g : Multiset α
a✝ : ∀ x ∈ 0, Prime x
hg : ∀ x ∈ g, Prime x
⊢ Multiset.prod 0 ~ᵤ g.prod → Multiset.Rel Associated 0 g

Tactic:
h

Goal state after:
case empty
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
g : Multiset α
a✝ : ∀ x ∈ 0, Prime x
hg : ∀ x ∈ g, Prime x
h : Multiset.prod 0 ~ᵤ g.prod
⊢ Multiset.Rel Associated 0 g
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case neg
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : f s = 0
⊢ f s ≤ ∑ x ∈ f.support, f x • w x

Tactic:
h

Goal state after:
case neg
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : f s = 0
⊢ 0 ≤ ∑ x ∈ f.support, f x • w x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Subsingleton Mˣ
x : M
⊢ factors x = normalizedFactors x

Tactic:
unfold normalizedFactors
  convert (Multiset.map_id (factors x)).symm with p
  exact normalize_eq p

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
⊢ normalizedFactors 1 = 0

Tactic:
rcases subsingleton_or_nontrivial α with h | h

Goal state after:
case inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Subsingleton α
⊢ normalizedFactors 1 = 0

case inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ normalizedFactors 1 = 0