mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ Fintype { l // l.Nodup }

Tactic:
refine Fintype.subtype ?_ ?_
  · let univSubsets := ((Finset.univ : Finset α).powerset.1 : (Multiset (Finset α)))
    let allPerms := Multiset.bind univSubsets (fun s => (Multiset.lists s.1))
    refine ⟨allPerms, Multiset.nodup_bind.mpr ?_⟩
    simp only [Multiset.lists_nodup_finset, implies_true, true_and]
    unfold Multiset.Pairwise
    use ((Finset.univ : Finset α).powerset.toList : (List (Finset α)))
    constructor
    · simp only [Finset.coe_toList]
      rfl
    · -- Unfold `List.Nodup` in the type of the proof term to make it match with the goal.
      convert dsimp% [List.Nodup] Finset.nodup_toList (Finset.univ.powerset : Finset (Finset α))
        with m n
      simp only [_root_.Disjoint]
      rw [← m.coe_toList, ← n.coe_toList, Multiset.lists_coe, Multiset.lists_coe]
      have := Multiset.coe_disjoint m.toList.permutations n.toList.permutations
      rw [_root_.Disjoint] at this
      rw [this, List.disjoint_iff_ne]
      constructor
      · intro h
        by_contra hc
        rw [hc] at h
        contrapose! h
        use n.toList
        simp
      · intro h
        simp only [mem_permutations]
        intro a ha b hb
        by_contra hab
        absurd h
        rw [hab] at ha
        exact Finset.perm_toList.mp <| Perm.trans ha.symm hb
  · intro l
    simp only [Finset.mem_mk, Multiset.mem_bind, Finset.mem_val, Finset.mem_powerset,
      Finset.subset_univ, Multiset.mem_lists_iff, Multiset.quot_mk_to_coe, true_and]
    constructor
    · intro h
      rcases h with ⟨f, hf⟩
      convert! f.nodup
      rw [hf]
      rfl
    · intro h
      exact CanLift.prf _ h

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

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
s : Set A
a✝ : A
hx : a✝ ∈ (Algebra.adjoin R (s ∪ star s)).carrier
⊢ a✝ ∈ Algebra.adjoin R (star s ∪ star (star s))

Tactic:
star_star,

Goal state after:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
s : Set A
a✝ : A
hx : a✝ ∈ (Algebra.adjoin R (s ∪ star s)).carrier
⊢ a✝ ∈ Algebra.adjoin R (star s ∪ s)
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
hf : IsPeriodicPt f n x
m : ℕ
⊢ IsFixedPt f^[n * m] x

Tactic:
iterate_mul

Goal state after:
α : Type u_1
f : α → α
x : α
n : ℕ
hf : IsPeriodicPt f n x
m : ℕ
⊢ IsFixedPt f^[n]^[m] x
Module: Mathlib.Data.List.Permutation

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

Tactic:
by
  rw [permutations, permutations, map, map_permutationsAux, map]

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

Goal state before:
pp: case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ f^[n / (minimalPeriod f x).gcd n * minimalPeriod f x] x = x

Tactic:
iterate_mul

Goal state after:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ f^[n / (minimalPeriod f x).gcd n]^[minimalPeriod f x] x = x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ f^[n * minimalPeriod f^[n] x] x = x

Tactic:
iterate_mul

Goal state after:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ f^[n]^[minimalPeriod f^[n] x] x = x
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
is l : List α
H : l ~ [] ++ is → (∃ ts' x, l = ts' ++ is) ∨ l ∈ is.permutationsAux []
⊢ l ~ is → l ∈ is.permutations

Tactic:
by simpa [permutations, perm_nil] using 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 % ↑(minimalPeriod (fun x ↦ a • x) b)) • b = a ^ n • b

Tactic:
by
  rw [← period_eq_minimalPeriod, zpow_mod_period_smul]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 ↦ decide (x = x_1)) l).length + 1
x : α
⊢ count (x :: y :: l) (permutations'Aux x (y :: l)) = (takeWhile (fun x_1 ↦ decide (x = x_1)) (y :: l)).length + 1

Tactic:
| cons y l IH =>

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
⊢ l.prev l[i] ⋯ = l[(i + (l.length - 1)) % l.length]

Tactic:
by
  grind [prev_eq_getElem]

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

Goal state before:
pp: α : Type u_1
x y : α
s : List α
⊢ take 2 (x :: y :: s).permutations = [x :: y :: s, y :: x :: s]

Tactic:
induction s <;> simp [permutations]

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

Goal state before:
pp: α : Type u_1
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
⊢ ↑l₁.cyclicPermutations = ↑l₂.cyclicPermutations

Tactic:
by
    simpa using h.cyclicPermutations.perm

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Surjective ⇑f
⊢ Nat.card G' ∣ Nat.card G

Tactic:
by
  rw [← Nat.card_congr (QuotientGroup.quotientKerEquivOfSurjective f hf).toEquiv]
  exact Dvd.intro_left (Nat.card f.ker) f.ker.card_mul_index

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : f.ker ≤ H
⊢ H.index ∣ (H ⊔ f.ker).index * f.range.index

Tactic:
sup_of_le_left hf

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : f.ker ≤ H
⊢ H.index ∣ H.index * f.range.index
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ZMod 0
⊢ n = 1 ∨ n = -1 ↔ n = ↑1 ∨ n = -↑1

Tactic:
Nat.cast_one

Goal state after:
n : ZMod 0
⊢ n = 1 ∨ n = -1 ↔ n = 1 ∨ n = -1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ↑↑k - ↑1 = ↑↑k - 1

pp: case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ 1 ≤ ↑k

Tactic:
Nat.cast_one

Goal state after:
case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ↑↑k - 1 = ↑↑k - 1

case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ 1 ≤ ↑k
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: hn : 1 ≠ 1
⊢ val 1 = 1

Tactic:
cases hn rfl

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

Goal state before:
pp: n : ℕ
a b : ZMod n
h : a.val + b.val < n
⊢ (a + b).val = a.val + b.val

Tactic:
by
  have : NeZero n := by constructor; rintro rfl; simp at h
  rw [ZMod.val_add, Nat.mod_eq_of_lt h]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case refine_1
m n : ℕ
hn : n ≠ 0
h : m ∈ n.properDivisors
⊢ n = m * (n / m)

Tactic:
exact (Nat.mul_div_cancel' (mem_properDivisors.mp h).1).symm

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

Goal state before:
pp: case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
hn : 0 ≠ 0
⊢ 0 < ∑ i ∈ range 0, x ^ i

Tactic:
cases hn rfl

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

Goal state before:
pp: n x : ℕ
h : (x % n).gcd n = 1
⊢ ↑1 = 1

Tactic:
Nat.cast_one

Goal state after:
n x : ℕ
h : (x % n).gcd n = 1
⊢ 1 = 1
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
⊢ ¬Odd n → ¬x + 1 ≤ 0

Tactic:
Nat.not_odd_iff_even

Goal state after:
case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
⊢ Even n → ¬x + 1 ≤ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = ↑1
⊢ (↑u)⁻¹ = ↑u⁻¹

Tactic:
Nat.cast_one

Goal state after:
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
⊢ (↑u)⁻¹ = ↑u⁻¹
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ -1
hn : 0 ≠ 0
⊢ ∑ i ∈ range 0, x ^ i ≠ 0

Tactic:
cases hn rfl

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

Goal state before:
pp: case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x ≠ -1
⊢ ∑ i ∈ range n, x ^ i ≠ 0

Tactic:
exact geom_sum_ne_zero hx hn

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mpr
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
⊢ ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n → n1 * n2 = n ∧ ¬n = 0

Tactic:
· intro ⟨⟨hn1, hn2⟩, hn3⟩
    exact ⟨hn3, n_ne_zero⟩

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

Goal state before:
pp: case neg.succ.zero
n : ℕ
lt : ¬n + 1 + 1 < 0
⊢ (n + 1 + 1).choose 0 ≤ 2 ^ (n + 1)

pp: case neg.succ.succ
n k : ℕ
lt : ¬n + 1 + 1 < k + 1
⊢ (n + 1 + 1).choose (k + 1) ≤ 2 ^ (n + 1)

Tactic:
· rw [choose_zero_right]
        exact Nat.one_le_two_pow

Goal state after:
case neg.succ.succ
n k : ℕ
lt : ¬n + 1 + 1 < k + 1
⊢ (n + 1 + 1).choose (k + 1) ≤ 2 ^ (n + 1)
Module: Mathlib.Data.Nat.Digits.Defs

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

Tactic:
convert! this

Goal state after:
case e'_2
b n : ℕ
h : b.digits n = []
this : ofDigits b (b.digits n) = ofDigits b []
⊢ n = ofDigits b (b.digits n)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) * ofDigits p tl + ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
← one_mul <| ofDigits p tl

Goal state after:
case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) * ofDigits p tl + 1 * ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c k : α
hc : b = a ^ multiplicity a b * a * k
hk : c = a * k
⊢ False

Tactic:
← _root_.pow_succ

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c k : α
hc : b = a ^ (multiplicity a b + 1) * k
hk : c = a * k
⊢ False
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✝ : Monoid G
a b x y : G
n m : ℕ
hx : IsOfFinOrder x
⊢ Group ↥(powers x)

Tactic:
obtain ⟨hpos, hx⟩ := hx.exists_pow_eq_one.choose_spec
  exact Submonoid.groupPowers hpos hx

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case hsucc
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ ¬p ^ (multiplicity p b + 1) ∣ a + b

Tactic:
dvd_add_right

Goal state after:
case hsucc
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ ¬p ^ (multiplicity p b + 1) ∣ b

case hsucc
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ p ^ (multiplicity p b + 1) ∣ a
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case pos
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : l = 0
⊢ ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
simp [hl, fixedLengthDigits_one, Finset.sum_range_id, choose_two_right]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Monoid G
x : G
n a : ℕ
hx : x ^ n = 1
c : ℕ
h : a ≡ a + n * c [MOD n]
hle : a ≤ a + n * c
⊢ x ^ a = x ^ (a + n * c)

Tactic:
simp [pow_add, pow_mul, hx]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Monoid G
x : G
n b : ℕ
hx : x ^ n = 1
c : ℕ
h : b + n * c ≡ b [MOD n]
hle : b ≤ b + n * c
⊢ x ^ (b + n * c) = x ^ b

Tactic:
simp [pow_add, pow_mul, hx]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a : α
hp : Prime p
k : ℕ
⊢ emultiplicity p (a ^ k) = ↑k * emultiplicity p a

Tactic:
by
  induction k with
  | zero => simp [emultiplicity_of_one_right hp.not_isUnit]
  | succ k hk => simp [pow_succ, emultiplicity_mul hp, hk, add_mul]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
pow_dvd_pow_iff h0 hu

Goal state after:
case hsucc
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ ¬n + 1 ≤ n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Monoid G
x : G
inst✝ : Monoid H
f : G →* H
hf : Injective ⇑f
⊢ IsOfFinOrder (f x) ↔ IsOfFinOrder x

Tactic:
rw [← orderOf_pos_iff, orderOf_injective f hf x, ← orderOf_pos_iff]

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

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

Tactic:
Nat.Prime.dvd_iff_one_le_factorization hp (ordCompl_pos p hn).ne'

Goal state after:
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬1 ≤ (n / p ^ n.factorization p).factorization p
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)!
⊢ ((n + k).choose k).factorization p + (k ! * n !).factorization p =
    #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}) + (k ! * n !).factorization p

Tactic:
← Pi.add_apply,

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

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

Tactic:
← Pi.add_apply,

Goal state after:
p n k : ℕ
hkn : k + 1 ≤ n + 1
hk : k + 1 ≠ 0
⊢ (n + 1).factorization p ≤ (⇑((n + 1).choose (k + 1)).factorization + ⇑(k + 1).factorization) p
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
hi₁ : 1 ≤ i
hi✝ : i < log p n + 1
hi : 1 < i
this : 3 ≤ p
⊢ 3 * p ≤ p * p

Tactic:
by gcongr

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
a : G
h : (↑(powers a)).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ a ^ (n - m) = 1

Tactic:
apply (mul_right_cancel_iff (a := a ^ m)).1

Goal state after:
G : Type u_1
inst✝ : RightCancelMonoid G
a : G
h : (↑(powers a)).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ a ^ (n - m) * a ^ m = 1 * a ^ m
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
by
  by_cases h : IsOfFinOrder x
  · rw [← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast, pow_orderOf_eq_one, one_zpow]
  · rw [orderOf_eq_zero h, _root_.pow_zero]

Goal state after:
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 ((p ^ n).choose k) + emultiplicity p k - ↑(multiplicity p k)

Tactic:
(finiteMultiplicity_iff.2 ⟨hp.ne_one, Nat.pos_of_ne_zero hk0⟩).emultiplicity_eq_multiplicity,

Goal state after:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p ((p ^ n).choose k) = emultiplicity p ((p ^ n).choose k) + ↑(multiplicity p k) - ↑(multiplicity p k)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt (fun x_1 ↦ x * x_1) w 1
⊢ x ^ w = 1

Tactic:
exact (isPeriodicPt_mul_iff_pow_eq_one _).mp hw2

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

Goal state before:
pp: p a b : ℕ
hab : a.Coprime b
hpb : p ∈ b.primeFactorsList
⊢ (a * b).factorization p = b.factorization p

Tactic:
rw [mul_comm]
  exact factorization_eq_of_coprime_left (coprime_comm.mp hab) hpb

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 : ℕ
⊢ (zpowersEquivZPowers h) ⟨x ^ n, ⋯⟩ = ⟨y ^ n, ⋯⟩

Tactic:
by
  rw [zpowersEquivZPowers, Equiv.trans_apply, Equiv.trans_apply, finEquivZPowers_symm_apply, ←
    Equiv.eq_symm_apply, finEquivZPowers_symm_apply]
  simp [h]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝ : Group G
s : Submonoid G
hs : (↑s).Finite
x : G
hx : x ∈ s
⊢ Nat.card ↥(powers x) ≤ Nat.card ↥s

Tactic:
exact Nat.card_mono hs <| powers_le.2 hx

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

Goal state before:
pp: case inl
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
x : k[G]
d : G
⊢ (single g 1 * x %ᵒᶠ g).coeff (g + d) = 0

Tactic:
coeff_modOf_self_add

Goal state after:
case inl
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
x : k[G]
d : G
⊢ 0 = 0
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case inl
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
x : k[G]
g d : G
⊢ (x * single g 1 %ᵒᶠ g).coeff (g + d) = 0

Tactic:
coeff_modOf_self_add

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

Goal state before:
pp: case pos
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : n = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
use b
    simp_all

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
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
rw [hp, zero_mul, trailingDegree_zero, top_add]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ (monomial n) (a * (↑n + ↑1)) = (monomial n) (a * (↑n + 1))

Tactic:
Nat.cast_one

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ (monomial n) (a * (↑n + 1)) = (monomial n) (a * (↑n + 1))
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬((expand R (p ^ n)) g).IsRoot r
| rootMultiplicity r ((expand R (p ^ n)) g) + p ^ n * rootMultiplicity (r ^ p ^ n) f

Tactic:
rootMultiplicity_eq_zero ndvd,

Goal state after:
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬((expand R (p ^ n)) g).IsRoot r
| 0 + p ^ n * rootMultiplicity (r ^ p ^ n) f
Module: Mathlib.RingTheory.Algebraic.Defs

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

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

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ (derivativeFinsupp p).support ⊆ range n

Tactic:
dsimp [derivativeFinsupp]
  exact Finsupp.support_onFinset_subset.trans (Finset.range_subset_range.mpr h)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ derivativeFinsupp 1 = Finsupp.single 0 1

Tactic:
by
  simpa using derivativeFinsupp_C (1 : R)

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

Goal state before:
pp: case refine_2.intro
α : 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 : Set ι
f : (i : ↑I) → ι' ↑i
hsub : ⋂ i, s (↑i) (⟨I, f⟩.snd i) ⊆ t
hI : ⟨I, f⟩.fst.Finite
hf : ∀ (i : ↑⟨I, f⟩.fst), p (↑i) (⟨I, f⟩.snd i)
val✝ : Fintype ↑⟨I, f⟩.fst
⊢ ⋂ i, s (↑i) (⟨I, f⟩.snd i) ∈ ⨅ i, l i

Tactic:
exact iInter_mem.2 fun i => mem_iInf_of_mem ↑i <| (hl i).mem_of_mem <| hf _

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

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

Tactic:
rcases h with ⟨t, hts, tfin, h⟩
    exact mem_of_superset ((sInter_mem tfin).2 fun V hV => GenerateSets.basic <| hts hV) h

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

Goal state before:
pp: α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
I_fin : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
hU : ⋂ i, V i ⊆ U
this : Fintype ↑I
i : ↑I
⊢ V i ∈ ⨅ i, s i

Tactic:
exact mem_iInf_of_mem (i : ι) (hV _)

Goal state after: