mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n m : ℕ
x✝¹ : m < ((List.map (fun n ↦ f^[n] x) (List.range (minimalPeriod f x))).rotate n).length
x✝ : m < (List.map (fun n_1 ↦ f^[n_1] (f^[n] x)) (List.range (minimalPeriod f (f^[n] x)))).length
⊢ ((List.map (fun n ↦ f^[n] x) (List.range (minimalPeriod f x))).rotate n).get ⟨m, x✝¹⟩ =
    (List.map (fun n_1 ↦ f^[n_1] (f^[n] x)) (List.range (minimalPeriod f (f^[n] x)))).get ⟨m, x✝⟩

Tactic:
by
      simp [List.getElem_rotate, iterate_add_apply]

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

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
| g ^ (j % ↑(period g a) + ↑(period g a) * (j / ↑(period g a))) • a

Tactic:
zpow_add,

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
| (g ^ (j % ↑(period g a)) * g ^ (↑(period g a) * (j / ↑(period g a)))) • a
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ ∀ {f g : α → α},
    Function.Commute f g → (minimalPeriod f x).Coprime (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x

Tactic:
intro f g h hco

Goal state after:
α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
⊢ minimalPeriod (Pi.map f) x = sInf {n | n > 0 ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}

Tactic:
by
  conv_lhs => simp [minimalPeriod_eq_sInf_n_pos_IsPeriodicPt]
  simp [← isPeriodicPt_iff_minimalPeriod_dvd]

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

Goal state before:
pp: case h.succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : l.Nodup
h✝ : (y :: l).getLast ⋯ ∈ l
h : (y :: l).getLast ⋯ ∈ y :: l
hy : (y :: l).getLast ⋯ ≠ y
H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast
k : ℕ
hk : k + 1 < (y :: l).dropLast.length
hk' : (y :: l).dropLast[k + 1] = (y :: l).getLast ⋯
⊢ k + 1 = l.length

Tactic:
rcases l with - | ⟨hd, tl⟩

Goal state after:
case h.succ.nil
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hl : [].Nodup
h✝ : [y].getLast ⋯ ∈ []
h : [y].getLast ⋯ ∈ [y]
hy : [y].getLast ⋯ ≠ y
H : [y].getLast ⋯ ∈ [y].dropLast
hk : k + 1 < [y].dropLast.length
hk' : [y].dropLast[k + 1] = [y].getLast ⋯
⊢ k + 1 = [].length

case h.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : (hd :: tl).Nodup
h✝ : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' : (y :: hd :: tl).dropLast[k + 1] = (y :: hd :: tl).getLast ⋯
⊢ k + 1 = (hd :: tl).length
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
⊢ s.insertIdx k x = s.insertIdx (k + 1) x

Tactic:
have hl : length (s.insertIdx k x) = length (s.insertIdx (k + 1) x) := by
    rw [length_insertIdx_of_le_length hk.le, length_insertIdx_of_le_length (Nat.succ_le_of_lt hk)]

Goal state after:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
hl : (s.insertIdx k x).length = (s.insertIdx (k + 1) x).length
⊢ s.insertIdx k x = s.insertIdx (k + 1) x
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : Semiring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : StarModule R A
ι : Type u_3
inst✝ : Nonempty ι
S : ι → StarSubalgebra R A
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ IsMulCommutative ↥(⨆ i, S i)

Tactic:
by
  simpa [isMulCommutative_iff, ← SetLike.mem_coe, coe_iSup_of_directed dir,
    Subalgebra.coe_iSup_of_directed dir] using Subalgebra.isMulCommutative_iSup dir

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : x ∈ l
⊢ l.prev x h ∈ l

Tactic:
rcases l with - | ⟨hd, tl⟩

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
x : α
h : x ∈ []
⊢ [].prev x h ∈ []

case cons
α : Type u_1
inst✝ : DecidableEq α
x hd : α
tl : List α
h : x ∈ hd :: tl
⊢ (hd :: tl).prev x h ∈ hd :: tl
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (as.insertIdx n x)[m] = x
hx' : (bs.insertIdx m x)[n] = x
ht : n < m
this : x ∈ bs
⊢ False

Tactic:
exact h x (hb.subset this) rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
⊢ l[(n + 1 + (l.length - 1)) % l.length] = l[n]

Tactic:
rcases l with - | ⟨hd, tl⟩

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
h : [].Nodup
hn : n < [].length
hx : [][n] ∈ []
⊢ [][(n + 1 + ([].length - 1)) % [].length] = [][n]

case cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn : n < (hd :: tl).length
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (hd :: tl)[(n + 1 + ((hd :: tl).length - 1)) % (hd :: tl).length] = (hd :: tl)[n]
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
⊢ l[(n + (l.length - 1) + 1) % l.length] = l[n]

Tactic:
rcases l with - | ⟨hd, tl⟩

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
h : [].Nodup
hn : n < [].length
hx : [][n] ∈ []
⊢ [][(n + ([].length - 1) + 1) % [].length] = [][n]

case cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn : n < (hd :: tl).length
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (hd :: tl)[(n + ((hd :: tl).length - 1) + 1) % (hd :: tl).length] = (hd :: tl)[n]
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case h
G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
a✝ : α
g : G
yh : (fun m ↦ m • a✝) g ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
h : G
zh : (fun m ↦ m • a✝) h ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
⊢ ∃ g_1, g_1 • ⟨(fun m ↦ m • a✝) g, yh⟩ = ⟨(fun m ↦ m • a✝) h, zh⟩

Tactic:
refine ⟨h * g⁻¹, ?_⟩

Goal state after:
case h
G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
a✝ : α
g : G
yh : (fun m ↦ m • a✝) g ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
h : G
zh : (fun m ↦ m • a✝) h ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
⊢ (h * g⁻¹) • ⟨(fun m ↦ m • a✝) g, yh⟩ = ⟨(fun m ↦ m • a✝) h, zh⟩
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
⊢ ∀ (a b : G), (leftRel H) a b → ⟦a⁻¹ • x⟧ = ⟦b⁻¹ • x⟧

Tactic:
intro g₁ g₂ h
    rw [leftRel_eq] at h
    rw [← @Quotient.mk''_eq_mk, Quotient.eq'', orbitRel_apply]
    exact ⟨⟨_, h⟩, by simp [mul_smul]⟩

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

Goal state before:
pp: n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
k : ℕ := n.primeFactorsList.length
⊢ n = p ^ k

Tactic:
← prod_primeFactorsList hpos,

Goal state after:
n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
k : ℕ := n.primeFactorsList.length
⊢ n.primeFactorsList.prod = p ^ k
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
n : ℕ
h : 0 = n + 1
⊢ ZMod 0 ≃+* ZMod (n + 1)

Tactic:
exfalso

Goal state after:
case zero.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
n : ℕ
h : 0 = n + 1
⊢ False
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.zero
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
m : ℕ
h : m + 1 = 0
⊢ ZMod (m + 1) ≃+* ZMod 0

Tactic:
exfalso

Goal state after:
case succ.zero
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
m : ℕ
h : m + 1 = 0
⊢ False
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a b : ℕ
⊢ ↑a = 0 ↔ b ∣ a

Tactic:
rw [← Nat.cast_zero, ZMod.natCast_eq_natCast_iff, Nat.modEq_zero_iff_dvd]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
intro ne_n

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
⊢ ∑ x ∈ (n + 1 + 1).properDivisors, x = 1
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_and,

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 → ¬x + 1 < 0
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inr
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
⊢ b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)

Tactic:
← ofDigits_digits_append_digits

Goal state after:
case inr
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
⊢ b.digits n ++ b.digits m = b.digits (ofDigits b (b.digits n ++ b.digits m))
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b : ℕ
l1 l2 : List ℕ
h : l1.length = l2.length
⊢ ofDigits b l1 + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) l1 l2)

Tactic:
induction l1 generalizing l2 with
  | nil => simp_all [eq_comm, List.length_eq_zero_iff, ofDigits]
  | cons hd₁ tl₁ ih₁ =>
    induction l2 generalizing tl₁ with
    | nil => simp_all
    | cons hd₂ tl₂ ih₂ =>
      simp_all only [List.length_cons, ofDigits_cons, add_left_inj,
        eq_comm, List.zipWith_cons_cons]
      rw [← ih₁ h.symm, mul_add]
      ac_rfl

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

Goal state before:
pp: case succ
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
⊢ b.digits (b ^ (k + 1) * m) = List.replicate (k + 1) 0 ++ b.digits m

Tactic:
rw [pow_succ', mul_assoc, digits_base_mul hb (by positivity), ih hm, List.replicate_succ,
      List.cons_append]

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

Goal state before:
pp: case inr
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p n.primeFactorsList = n.factorization p

Tactic:
simp only [factorization_def _ pp]

Goal state after:
case inr
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p n.primeFactorsList = padicValNat p n
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n : ℕ
⊢ n.factorization = Multiset.toFinsupp ↑n.primeFactorsList

Tactic:
ext p

Goal state after:
n p : ℕ
⊢ n.factorization p = (Multiset.toFinsupp ↑n.primeFactorsList) p
Module: Mathlib.Data.Nat.Factorization.Defs

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

Tactic:
rw [factorization_eq_primeFactorsList_multiset n]

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ ((Multiset.toFinsupp ↑n.primeFactorsList).prod fun x1 x2 ↦ x1 ^ x2) = n
Module: Mathlib.Data.Nat.Factorization.Defs

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

Tactic:
ext p

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (a * b).factorization p = (a.factorization + b.factorization) p
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
Finset.sum_add_distrib,

Goal state after:
case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ ∑ x ∈ fixedLengthDigits hb l, ∑ x ∈ Finset.range b, x + ∑ x ∈ fixedLengthDigits hb l, ∑ x_1 ∈ Finset.range b, x.sum =
    (l + 1) * b ^ (l + 1 - 1) * b.choose 2
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ p ^ n.factorization p ∣ n

Tactic:
rw [← primeFactorsList_count_eq]

Goal state after:
n p : ℕ
hp : Prime p
⊢ p ^ count p n.primeFactorsList ∣ n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n : ℕ
⊢ n.factorization = 0 ↔ n = 0 ∨ n = 1

Tactic:
rw [factorization_eq_primeFactorsList_multiset n]

Goal state after:
n : ℕ
⊢ Multiset.toFinsupp ↑n.primeFactorsList = 0 ↔ n = 0 ∨ n = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
inst✝ : Subsingleton Gˣ
x : G
h : IsUnit x
⊢ orderOf x = 1

Tactic:
simp [isUnit_iff_eq_one.mp h]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
⊢ (closure s).toSubmonoid = Submonoid.closure s

Tactic:
by
  refine le_antisymm ?_ (le_closure_toSubmonoid s)
  rw [closure_toSubmonoid]
  refine Submonoid.closure_le.mpr <| Set.union_subset Submonoid.subset_closure
    fun x (hx : x⁻¹ ∈ s) ↦ ?_
  apply Submonoid.powers_le.mpr (Submonoid.subset_closure hx)
  simp [(hs _ hx).mem_powers_iff_mem_zpowers]

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

Goal state before:
pp: case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support
hp1 : p ∈ {p ∈ Finset.range m | Prime p}
hp2 : p ∉ n.factorization.support
⊢ p ^ padicValNat p n = 1

Tactic:
rw [← factorization_def n (Finset.mem_filter.mp hp1).2]

Goal state after:
case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support
hp1 : p ∈ {p ∈ Finset.range m | Prime p}
hp2 : p ∉ n.factorization.support
⊢ p ^ n.factorization p = 1
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 + ↑n * (Nat.card G).gcdB n)
⊢ (fun g ↦ g ^ (Nat.card G).gcdB n) ((fun g ↦ g ^ n) g) = g

Tactic:
zpow_add,

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 ^ (↑n * (Nat.card G).gcdB n)
⊢ (fun g ↦ g ^ (Nat.card G).gcdB n) ((fun g ↦ g ^ n) g) = g
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 + ↑n * (Nat.card G).gcdB n)
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g

Tactic:
zpow_add,

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 ^ (↑n * (Nat.card G).gcdB n)
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝ : NonAssocRing R
n : ℕ
⊢ ↑n = 0 ↔ addOrderOf 1 ∣ n

Tactic:
rw [← Nat.smul_one_eq_cast, addOrderOf_dvd_iff_nsmul_eq_zero]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r : R
⊢ eval r ((expand R p) P) = eval (r ^ p) P

Tactic:
by
  refine Polynomial.induction_on P (fun a => by simp) (fun f g hf hg => ?_) fun n a _ => by simp
  rw [map_add, eval_add, eval_add, hf, hg]

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:
coeff_iterate_derivative,

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
⊢ map f x ∣ map f y ↔ x ∣ y

Tactic:
← modByMonic_eq_zero_iff_dvd hx,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
⊢ map f x ∣ map f y ↔ y %ₘ x = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
⊢ eval a (p /ₘ (X - C a) ^ rootMultiplicity a p) ≠ 0

Tactic:
classical
  have : Nontrivial R := Nontrivial.of_polynomial_ne hp
  rw [Ne, ← IsRoot, ← dvd_iff_isRoot]
  rintro ⟨q, hq⟩
  have := pow_mul_divByMonic_rootMultiplicity_eq p a
  rw [hq, ← mul_assoc, ← pow_succ, rootMultiplicity_eq_multiplicity, if_neg hp] at this
  exact
    (finiteMultiplicity_of_degree_pos_of_monic
      (show (0 : WithBot ℕ) < degree (X - C a) by rw [degree_X_sub_C]; decide)
      (monic_X_sub_C _) hp).not_pow_dvd_of_multiplicity_lt
      (Nat.lt_succ_self _) (dvd_of_mul_right_eq _ this)

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

Goal state before:
pp: α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i ↦ U ∪ ⋂₀ σ i
hV : V = fun i ↦ U ∪ ⋂₀ σ i
i : ↑I
this : ⋂₀ σ i ∈ s ↑i
⊢ V i ∈ s ↑i

Tactic:
exact mem_of_superset this subset_union_right

Goal state after:
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).pred ∣ (⇑derivative ∘ (⇑derivative)^[m]) p

Tactic:
exact pow_sub_one_dvd_derivative_of_pow_dvd (ih dvd)

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
n m : ℕ
dvd : q ^ n ∣ p
⊢ q ^ (n - m) ∣ (⇑derivative)^[m] p

Tactic:
by
  induction m generalizing p with
  | zero => simpa
  | succ m ih =>
    rw [Nat.sub_succ, Function.iterate_succ']
    exact pow_sub_one_dvd_derivative_of_pow_dvd (ih dvd)

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
l : Filter β
⊢ Tendsto m l (pi f) ↔ ∀ (i : ι), Tendsto (fun x ↦ m x i) l (f i)

Tactic:
by
  simp only [pi, tendsto_iInf, tendsto_comap_iff]; rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
⊢ (g.comp (X + C t)).coeff 0 = eval t g

Tactic:
coeff_zero_eq_eval_zero,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
⊢ eval 0 (g.comp (X + C t)) = eval t g
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case zero
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
h : ∀ m < 0, (X - C a) ^ (m + 1) ∣ p
⊢ (X - C a) ^ 0 ∣ p

Tactic:
rw [pow_zero]
    apply one_dvd

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ rootMultiplicity x p + rootMultiplicity x q ≤ rootMultiplicity x (p * q)

Tactic:
rw [le_rootMultiplicity_iff hpq, pow_add]
  gcongr <;> apply pow_rootMultiplicity_dvd

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_4
s : (i : ι) → Set (α i)
l : (i : ι) → Filter (α i)
h : ∀ (i : ι), s i ∈ l i
hfin : ∀ᶠ (i : ι) in cofinite, s i = univ
⊢ univ.pi s ∈ pi l

Tactic:
filter_upwards [pi_mem_pi hfin fun i _ ↦ h i] with a ha i _
  if hi : s i = univ then
    simp [hi]
  else
    exact ha i hi

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

Goal state before:
pp: α : Type u_2
f : Filter α
⊢ f.ker = ∅ ↔ f ≤ ￢f

Tactic:
Filter.hnot_def,

Goal state after:
α : Type u_2
f : Filter α
⊢ f.ker = ∅ ↔ f ≤ 𝓟 f.kerᶜ
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case refine_4.refine_2
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ q.2 ≤ ￢f

Tactic:
Filter.hnot_def,

Goal state after:
case refine_4.refine_2
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ q.2 ≤ 𝓟 f.kerᶜ
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Semiring R
w : σ → M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hw : ∀ (i : σ), w i ≠ 0
n : R
s : σ
h : n • w s = 0
⊢ n = 0

Tactic:
by
    rw [smul_eq_zero, or_iff_not_imp_right] at h
    exact h (hw s)

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

Goal state before:
pp: σ : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Semiring R
w : σ → M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NonTorsionWeight R w
s : σ
h : w s = 0
⊢ False

Tactic:
by
  rw [← one_smul R (w s)] at h
  apply zero_ne_one.symm (α := R)
  exact NonTorsionWeight.eq_zero_of_smul_eq_zero h

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

Goal state before:
pp: R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ a ∈ p.roots ↔ p ≠ 0 ∧ p.IsRoot a

Tactic:
← count_pos,

Goal state after:
R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ 0 < count a p.roots ↔ p ≠ 0 ∧ p.IsRoot a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ ∀ p ∈ normalizedFactors a, ∀ q ∈ normalizedFactors a, p ∣ q → p = q

Tactic:
by
  intro p hp q hq hdvd
  convert!
    normalize_eq_normalize hdvd
      ((prime_of_normalized_factor _ hp).irreducible.dvd_symm
        (prime_of_normalized_factor _ hq).irreducible hdvd) <;>
    apply (normalize_normalized_factor _ ‹_›).symm

Goal state after: