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

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
a b : MvPolynomial σ R
hd : C r ∣ a * b
⊢ C r ∣ a ∨ C r ∣ b

Tactic:
obtain ⟨s, a', b', rfl, rfl⟩ := exists_finset_rename₂ a b
      rw [← algebraMap_eq] at hd
      have : algebraMap R _ r ∣ a' * b' := by
        convert! _root_.map_dvd (killCompl Subtype.val_injective) hd
        · simp
        · simp
      rw [← rename_C ((↑) : s → σ)]
      let f := (rename (R := R) ((↑) : s → σ)).toRingHom
      exact (((prime_C_iff_of_fintype s).2 hr).2.2 a' b' this).imp (map_dvd f) (map_dvd f)

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: a b : ℤ
⊢ a ≡ b [ZMOD 0] ↔ a = b

Tactic:
rw [ModEq, emod_zero, emod_zero]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
x : R
⊢ (quotientKerEquivOfSurjective hf).symm (f x) = (Ideal.Quotient.mk (ker f)) x

Tactic:
by
  apply (RingHom.quotientKerEquivOfSurjective hf).injective
  simp

Goal state after:
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: case inr.inr.inr.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : -1 = 1
⊢ -1 = 1

Tactic:
exact ((Ring.neg_one_ne_one_of_char_ne_two hR) h).elim

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

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : Field R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
hr : r ≠ 0
hr' : (algebraMap R A) r ∈ s
⊢ False

Tactic:
Algebra.algebraMap_eq_smul_one

Goal state after:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : Field R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
hr : r ≠ 0
hr' : r • 1 ∈ s
⊢ False
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ 2 ∣ p ↔ p = 2

Tactic:
prime_dvd_prime_iff_eq prime_two hp,

Goal state after:
p : ℕ
hp : Prime p
⊢ 2 = p ↔ p = 2
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case mk.mk
A : Type u_3
inst✝³ : Ring A
R : Type u_5
inst✝² : CommRing R
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : Algebra R A
a₁✝ : R ⧸ comap (algebraMap R A) I
a : R
a₂✝ : R ⧸ comap (algebraMap R A) I
b : R
hab : (algebraMap R A) (a - b) ∈ I
⊢ Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) a =
    Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) b

Tactic:
exact Quotient.eq.mpr hab

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

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

Tactic:
rcases xs with - | ⟨z, zs⟩

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
y x d : α
h : x ≠ y
⊢ [y].nextOr x d = [].nextOr x d

case cons
α : Type u_1
inst✝ : DecidableEq α
y x d : α
h : x ≠ y
z : α
zs : List α
⊢ (y :: z :: zs).nextOr x d = (z :: zs).nextOr x d
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
m : M
a : α
⊢ m ^ period m a • a = a

Tactic:
period_eq_minimalPeriod,

Goal state after:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
m : M
a : α
⊢ m ^ minimalPeriod (fun x ↦ m • x) a • a = a
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
⊢ m ^ n • a = a ↔ period m a ∣ n

Tactic:
period_eq_minimalPeriod,

Goal state after:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
⊢ m ^ n • a = a ↔ minimalPeriod (fun x ↦ m • x) a ∣ n
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
⊢ m ^ (period m a + n) • a = m ^ n • a

Tactic:
by
  rw [← pow_mod_period_smul, Nat.add_mod_left, pow_mod_period_smul]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : x ∈ l.dropLast
y : α
hy : x ≠ y
⊢ (y :: l).next x ⋯ = l.next x ⋯

Tactic:
by
  rwa [next, next, nextOr_cons_of_ne _ _ _ _ hy, nextOr_eq_nextOr_of_mem_dropLast]

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

Goal state before:
pp: α : Type u_1
s : List α
x : α
h : (permutations'Aux x s).Nodup
H : x ∈ s
⊢ False

Tactic:
obtain ⟨⟨k, hk⟩, hk'⟩ := get_of_mem H

Goal state after:
α : Type u_1
s : List α
x : α
h : (permutations'Aux x s).Nodup
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
⊢ False
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x ≠ z
h : x ∈ [y, z]
⊢ [y, z].prev x h = [z].prev x ⋯

pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x ≠ z
head✝ : α
tail✝ : List α
h : x ∈ y :: z :: head✝ :: tail✝
⊢ (y :: z :: head✝ :: tail✝).prev x h = (z :: head✝ :: tail✝).prev x ⋯

Tactic:
· simp [hy, hz] at h

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x ≠ z
head✝ : α
tail✝ : List α
h : x ∈ y :: z :: head✝ :: tail✝
⊢ (y :: z :: head✝ :: tail✝).prev x h = (z :: head✝ :: tail✝).prev x ⋯
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
⊢ swap a b ∈ MulAction.stabilizer (Perm α) S ↔ (a ∈ S ↔ b ∈ S)

Tactic:
rw [MulAction.mem_stabilizer_iff, Set.ext_iff, ← swap_inv]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
⊢ (∀ (x : α), x ∈ (swap a b)⁻¹ • S ↔ x ∈ S) ↔ (a ∈ S ↔ b ∈ S)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
l : List β
⊢ Chain r (map f ⟦l⟧) ↔ Chain (fun a b ↦ r (f a) (f b)) ⟦l⟧

Tactic:
rcases l with - | ⟨a, l⟩

Goal state after:
case nil
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
⊢ Chain r (map f ⟦[]⟧) ↔ Chain (fun a b ↦ r (f a) (f b)) ⟦[]⟧

case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ Chain r (map f ⟦a :: l⟧) ↔ Chain (fun a b ↦ r (f a) (f b)) ⟦a :: l⟧
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a✝ : ℕ
⊢ a✝ ∈ (a * b).primeFactors ↔ a✝ ∈ a.primeFactors ∪ b.primeFactors

Tactic:
simp only [Finset.mem_union, mem_primeFactors_iff_mem_primeFactorsList,
    mem_primeFactorsList_mul ha hb]

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

Goal state before:
pp: case succ.mp
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
u : List ℕ
hu1 : u ~ b.primeFactorsList
hu2 : replicate (n + 1) a <+ u
⊢ a ^ (n + 1) ∣ b

Tactic:
← Nat.prod_primeFactorsList hb,

Goal state after:
case succ.mp
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
u : List ℕ
hu1 : u ~ b.primeFactorsList
hu2 : replicate (n + 1) a <+ u
⊢ a ^ (n + 1) ∣ b.primeFactorsList.prod
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ a, ∀ (b : G), Xor (b * a ∈ H) (b ∈ H)) ↔ ∃ a, ∀ (b : G), Xor (a * b ∈ H) (b ∈ H)

Tactic:
(Equiv.inv G).exists_congr

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ b, ?m.40 b) ↔ ∃ a, ∀ (b : G), Xor (a * b ∈ H) (b ∈ H)

G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (a : G), (∀ (b : G), Xor (b * a ∈ H) (b ∈ H)) ↔ ?m.40 ((Equiv.inv G) a)

G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ G → Prop
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Tactic:
by_cases ha : a ∈ H

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ a, ∀ (b : G), b * a ∈ H ∨ b ∈ H) ↔ ∃ a, ∀ (b : G), a * b ∈ H ∨ b ∈ H

Tactic:
(Equiv.inv G).exists_congr

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ b, ?m.43 b) ↔ ∃ a, ∀ (b : G), a * b ∈ H ∨ b ∈ H

G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (a : G), (∀ (b : G), b * a ∈ H ∨ b ∈ H) ↔ ?m.43 ((Equiv.inv G) a)

G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ G → Prop
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(↑a).val
⊢ ↑(↑a).val = a % ↑n

Tactic:
have hlt : ↑(a : ZMod n).val < (n : ℤ) := Int.ofNat_lt.mpr (ZMod.val_lt a)

Goal state after:
n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(↑a).val
hlt : ↑(↑a).val < ↑n
⊢ ↑(↑a).val = a % ↑n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a b : ZMod n
⊢ (a * b).val ≤ a.val * b.val

Tactic:
by
  rw [val_mul]
  apply Nat.mod_le

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n

Tactic:
by
  rcases Decidable.eq_or_ne n 0 with (rfl | hn)
  · simp
  · rw [← cons_self_properDivisors hn, Finset.sum_cons, add_comm]

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

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

Tactic:
← mul_inv_eq_gcd,

Goal state after:
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = ↑1
⊢ (↑u)⁻¹ = ↑u⁻¹
Module: Mathlib.Data.ZMod.Basic

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

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

Tactic:
· simp [ZMod]

Goal state after:
case mp.succ.succ
n : ℕ
⊢ Subsingleton (ZMod (n + 1 + 1)) → n + 1 + 1 = 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: xy : ℤ × ℤ
z : ℤ
⊢ xy.swap ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag

Tactic:
by
  simp [mul_comm]

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

Goal state before:
pp: case inl
k : ℕ
⊢ choose 0 k ≤ 2 ^ 0

Tactic:
cases k <;> simp

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

Goal state before:
pp: b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ 0 < l.getLast hl

Tactic:
pos_iff_ne_zero

Goal state after:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ l.getLast hl ≠ 0
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: p q : ℕ
L : List ℕ
h : p ≤ q
⊢ ofDigits p L ≤ ofDigits q L

Tactic:
by
  induction L with
  | nil => rfl
  | cons _ _ hi =>
    simp only [ofDigits, cast_id, add_le_add_iff_left]
    exact Nat.mul_le_mul h hi

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
⊢ x ^ orderOf x = 1

Tactic:
convert! Eq.trans _ (isPeriodicPt_minimalPeriod (x * ·) 1)
  rw [orderOf, mul_left_iterate_apply_one]

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ (b.digits (ofDigits b L)).sum = (b.digitsAppend l (ofDigits b L)).sum

Tactic:
rw [digitsAppend, List.sum_append_nat, List.sum_replicate, nsmul_zero, add_zero]

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l d : ℕ
L : List ℕ
hL : L ∈ consFixedLengthDigits hb l d
⊢ L ≠ []

Tactic:
obtain ⟨_, _, rfl⟩ := Finset.mem_image.mp hL

Goal state after:
b : ℕ
hb : 1 < b
l d : ℕ
w✝ : List ℕ
left✝ : w✝ ∈ fixedLengthDigits hb l
hL : d :: w✝ ∈ consFixedLengthDigits hb l d
⊢ d :: w✝ ≠ []
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l d : ℕ
L : List ℕ
hL : L ∈ consFixedLengthDigits hb l d
⊢ L ≠ []

Tactic:
obtain ⟨_, _, rfl⟩ := Finset.mem_image.mp hL
  exact cons_ne_nil d _

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l d : ℕ
L : List ℕ
hL : L ∈ consFixedLengthDigits hb l d
⊢ L.head ⋯ = d

Tactic:
obtain ⟨_, _, rfl⟩ := Finset.mem_image.mp hL

Goal state after:
b : ℕ
hb : 1 < b
l d : ℕ
w✝ : List ℕ
left✝ : w✝ ∈ fixedLengthDigits hb l
hL : d :: w✝ ∈ consFixedLengthDigits hb l d
⊢ (d :: w✝).head ⋯ = d
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
⊢ 0 < orderOf x ↔ ¬orderOf x = 0

Tactic:
pos_iff_ne_zero

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
⊢ orderOf x ≠ 0 ↔ ¬orderOf x = 0
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
⊢ multiplicity a a = 1

Tactic:
by_cases ha : FiniteMultiplicity a a

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
⊢ multiplicity a a = 1

case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : ¬FiniteMultiplicity a a
⊢ multiplicity a a = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ x ^ (n / a.minFac) = 1

Tactic:
rw [← orderOf_dvd_iff_pow_eq_one, Nat.dvd_div_iff_mul_dvd a_min_fac_dvd_p_sub_one, ha, mul_comm,
    Nat.mul_dvd_mul_iff_left (IsOfFinOrder.orderOf_pos _)]

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ a.minFac ∣ a

G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ IsOfFinOrder x
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case succ
p n✝ n : ℕ
hn : n < p → n !.factorization p = 0
h : n + 1 < p
⊢ (n + 1)!.factorization p = 0

Tactic:
| succ n hn =>

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

Goal state before:
pp: case succ
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
m : ℕ
hm : m + 1 ≠ 1
hb : log (m + 1) n < b
fin : FiniteMultiplicity (m + 1) n
h : (m + 1) ^ i ∣ n
⊢ i < b

Tactic:
refine LE.le.trans_lt ?_ hb

Goal state after:
case succ
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
m : ℕ
hm : m + 1 ≠ 1
hb : log (m + 1) n < b
fin : FiniteMultiplicity (m + 1) n
h : (m + 1) ^ i ∣ n
⊢ i ≤ log (m + 1) n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
hx : IsOfFinOrder x
n : ℕ
⊢ ((finEquivPowers hx).trans (Equiv.setCongr ⋯)).symm ⟨x ^ n, ⋯⟩ = ⟨n % orderOf x, ⋯⟩

Tactic:
Equiv.symm_trans_apply

Goal state after:
G : Type u_1
inst✝ : Group G
x : G
hx : IsOfFinOrder x
n : ℕ
⊢ (finEquivPowers hx).symm ((Equiv.setCongr ⋯).symm ⟨x ^ n, ⋯⟩) = ⟨n % orderOf x, ⋯⟩
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
⊢ (_root_.iterateFrobenius S p n) (f • s) =
    (_root_.iterateFrobenius R p n) f • (↑↑(_root_.iterateFrobenius S p n)).toFun s

Tactic:
simp_rw [iterateFrobenius_def, Algebra.smul_def, mul_pow, ← map_pow]; rfl

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

Goal state before:
pp: case succ
p n : ℕ
hn : #({e ∈ Finset.range n | p ∣ e + 1}) = n / p
⊢ #({e ∈ Finset.range (n + 1) | p ∣ e + 1}) = (n + 1) / p

Tactic:
| succ n hn =>

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

Goal state before:
pp: case pos.h₀
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ f.support
hb2 : b ≠ n / p
⊢ (if p * b = n then f.coeff b else 0) = 0

Tactic:
rw [if_neg]

Goal state after:
case pos.h₀.hnc
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ f.support
hb2 : b ≠ n / p
⊢ ¬p * b = n
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
a✝ : k ∈ f.support
⊢ (if p * k = n then f.coeff k else 0) = 0

Tactic:
rw [if_neg]

Goal state after:
case neg.hnc
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
a✝ : k ∈ f.support
⊢ ¬p * k = n
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
⊢ X ^ (n + 1) ∣ f

Tactic:
| succ n hn =>

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ rootMultiplicity t p = rootMultiplicity 0 (p.comp (X + C t))

Tactic:
rootMultiplicity_eq_multiplicity,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ (if p = 0 then 0 else multiplicity (X - C t) p) =
    if p.comp (X + C t) = 0 then 0 else multiplicity (X - C 0) (p.comp (X + C t))
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ rootMultiplicity t p = rootMultiplicity 0 (p.comp (X + C t))

Tactic:
simp_rw [rootMultiplicity_eq_multiplicity, comp_X_add_C_eq_zero_iff]

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ (if p = 0 then 0 else multiplicity (X - C t) p) = if p = 0 then 0 else multiplicity (X - C 0) (p.comp (X + C t))
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg.refine_2
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ ((expand R p) f).coeff (f.natDegree * p) ≠ 0

Tactic:
rw [coeff_expand_mul hp, ← leadingCoeff]

Goal state after:
case neg.refine_2
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ f.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 0
⊢ derivative p = 0

Tactic:
by
  rw [eq_C_of_natDegree_eq_zero hp, derivative_C]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
ha : a ≠ 0
hab : IsRelPrime a b
⊢ Irreducible (C a * X + C b)

Tactic:
by
  apply irreducible_of_degree_eq_one_of_isRelPrime_coeff
  · compute_degree!
  · simpa using hab.symm

Goal state after:
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
⊢ (∀ x ∈ S, IsAlgebraic R x) ↔ Algebra.IsAlgebraic R ↥S

Tactic:
Subtype.forall',

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (∀ (x : ↥S), IsAlgebraic R ↑x) ↔ Algebra.IsAlgebraic R ↥S
Module: Mathlib.Algebra.Polynomial.CancelLeads

Goal state before:
pp: case a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = q.natDegree
⊢ C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0

Tactic:
← leadingCoeff_eq_zero,

Goal state after:
case a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = q.natDegree
⊢ (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).leadingCoeff = 0
Module: Mathlib.Algebra.Polynomial.CancelLeads

Goal state before:
pp: case a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = q.natDegree
⊢ p.leadingCoeff * q.coeff (p.natDegree + (q.natDegree - p.natDegree)) + -(q.leadingCoeff * p.coeff p.natDegree) = 0

Tactic:
add_comm p.natDegree,

Goal state after:
case a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = q.natDegree
⊢ p.leadingCoeff * q.coeff (q.natDegree - p.natDegree + p.natDegree) + -(q.leadingCoeff * p.coeff p.natDegree) = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ i ∈ range n.succ, (n + 1).choose (i + 1) • ((⇑derivative)^[n + 1 - (i + 1)] p * (⇑derivative)^[i + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q) =
    ∑ k ∈ range n.succ.succ, n.succ.choose k • ((⇑derivative)^[n.succ - k] p * (⇑derivative)^[k] q)

Tactic:
sum_range_succ' _ n.succ,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ i ∈ range n.succ, (n + 1).choose (i + 1) • ((⇑derivative)^[n + 1 - (i + 1)] p * (⇑derivative)^[i + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q) =
    ∑ k ∈ range n.succ, n.succ.choose (k + 1) • ((⇑derivative)^[n.succ - (k + 1)] p * (⇑derivative)^[k + 1] q) +
      n.succ.choose 0 • ((⇑derivative)^[n.succ - 0] p * (⇑derivative)^[0] q)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr.refine_2
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n
⊢ (p /ₘ (X - C a)).coeff p.natDegree = ∑ i ∈ Icc (p.natDegree + 1) p.natDegree, a ^ (i - (p.natDegree + 1)) * p.coeff i

Tactic:
· exact this _ le_rfl

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

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

Tactic:
rootMultiplicity_eq_multiplicity,

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : ¬p = 0
⊢ ((X - C a) ^ if p = 0 then 0 else multiplicity (X - C a) p) ∣ p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
hp : p ≠ 0
a : R
⊢ ∃ q, p = (X - C a) ^ rootMultiplicity a p * q ∧ ¬X - C a ∣ q

Tactic:
rootMultiplicity_eq_multiplicity,

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
hp : p ≠ 0
a : R
⊢ ∃ q, p = ((X - C a) ^ if p = 0 then 0 else multiplicity (X - C a) p) * q ∧ ¬X - C a ∣ q
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case bot
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
⊢ ⊥ < 1 → ⊥ ≤ 0

pp: case coe
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝¹ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
a✝ : ℕ
⊢ ↑a✝ < 1 → ↑a✝ ≤ 0

Tactic:
· exact fun _ => bot_le

Goal state after:
case coe
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝¹ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
a✝ : ℕ
⊢ ↑a✝ < 1 → ↑a✝ ≤ 0