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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝² : AddCommMonoid M
x✝¹ : Module R M
x✝ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝ : AddCommGroup M := addCommMonoidToAddCommGroup R
this : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
⊢ n = 0

Tactic:
let N' := span A ({n} ∪ Set.range nj)

Goal state after:
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝² : AddCommMonoid M
x✝¹ : Module R M
x✝ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝ : AddCommGroup M := addCommMonoidToAddCommGroup R
this : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
⊢ n = 0
Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ toSubmodule S * toSubmodule T ≤ toSubmodule (S ⊔ T)

Tactic:
rw [Submodule.mul_le]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ ∀ m ∈ toSubmodule S, ∀ n ∈ toSubmodule T, m * n ∈ toSubmodule (S ⊔ T)
Module: Mathlib.Algebra.Algebra.Subalgebra.Rank

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
h✝ : Subsingleton R
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A ↑B)

Tactic:
have := Module.subsingleton R S

Goal state after:
case inl
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
h✝ : Subsingleton R
this : Subsingleton S
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A ↑B)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.refine_1
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ x ∈ ⇑C '' ↑I, ∀ (m : σ →₀ ℕ), coeff m x ∈ I

Tactic:
intro f hf n
      obtain ⟨x, hx⟩ := (Set.mem_image _ _ _).mp hf
      rw [← hx.right, coeff_C]
      by_cases h : n = 0
      · simpa [h] using hx.left
      · simp [Ne.symm h]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
⊢ f ∈ Ideal.map C I → ∀ (m : σ →₀ ℕ), coeff m f ∈ I

pp: case mpr
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
⊢ (∀ (m : σ →₀ ℕ), coeff m f ∈ I) → f ∈ Ideal.map C I

Tactic:
· intro hf
    refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
    · intro f hf n
      obtain ⟨x, hx⟩ := (Set.mem_image _ _ _).mp hf
      rw [← hx.right, coeff_C]
      by_cases h : n = 0
      · simpa [h] using hx.left
      · simp [Ne.symm h]
    · simp
    · exact fun f g _ _ hf hg n => by simp [I.add_mem (hf n) (hg n)]
    · intro f g _ hg n
      rw [smul_eq_mul, coeff_mul]
      exact I.sum_mem fun c _ => I.mul_mem_left (f.coeff c.fst) (hg c.snd)

Goal state after:
case mpr
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
⊢ (∀ (m : σ →₀ ℕ), coeff m f ∈ I) → f ∈ Ideal.map C I
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
v : R
hu : (Ideal.Quotient.lift I f H) ((Ideal.Quotient.mk I) v) = 0
⊢ (Ideal.Quotient.mk I) v = 0

Tactic:
rw [Ideal.Quotient.lift_mk] at hu

Goal state after:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
v : R
hu : f v = 0
⊢ (Ideal.Quotient.mk I) v = 0
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
hgcd : a.gcd b = 1
⊢ ↑(a.gcd b) ≡ 1 [ZMOD ↑b]

Tactic:
hgcd

Goal state after:
a b : ℕ
hab : a.Coprime b
hgcd : a.gcd b = 1
⊢ ↑1 ≡ 1 [ZMOD ↑b]
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : IsRightCancelAdd R
⊢ InjOn Int.cast (Ico 0 ↑p)

Tactic:
by
  rintro a ⟨ha₀, ha⟩ b ⟨hb₀, hb⟩ hab
  lift a to ℕ using ha₀
  lift b to ℕ using hb₀
  norm_cast at *
  exact natCast_injOn_Iio _ _ ha hb hab

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

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
A : Type u_3
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
algHom : Unitization R ↥s →ₐ[R] ↥(Algebra.adjoin R ↑s) := (unitization s).codRestrict (Algebra.adjoin R ↑s) ⋯
this : Function.Injective (⇑(Algebra.adjoin R ↑s).val ∘ ⇑algHom)
⊢ Function.Injective ⇑algHom

Tactic:
exact this.of_comp

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

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : Field R
inst✝⁶ : StarRing R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : StarModule R A
inst✝¹ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R ↑s) :=
  (unitization s).codRestrict (StarAlgebra.adjoin R ↑s) ⋯
this : Function.Injective (⇑(StarAlgebra.adjoin R ↑s).subtype ∘ ⇑starAlgHom)
⊢ Function.Injective ⇑starAlgHom

Tactic:
exact this.of_comp

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

Goal state before:
pp: case mp
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ Bijective ⇑(mk I) → I = ⊥

Tactic:
intro h
    rw [← map_eq_bot_iff_of_injective h.1]
    exact (map_eq_bot_iff_le_ker _).mpr <| le_of_eq mk_ker.symm

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

Goal state before:
pp: R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
⊢ factorₐ R ⋯ = AlgHom.id R (A ⧸ I)

Tactic:
by
  ext
  simp

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

Goal state before:
pp: p : ℕ
pp : Prime p
m i : ℕ
⊢ i ∣ p ^ m ↔ ∃ k, k ≤ m ∧ i = p ^ k

Tactic:
_root_.dvd_prime_pow (prime_iff.mp pp) m,

Goal state after:
p : ℕ
pp : Prime p
m i : ℕ
⊢ (∃ i_1, i_1 ≤ m ∧ Associated i (p ^ i_1)) ↔ ∃ k, k ≤ m ∧ i = p ^ k
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : Type u_1
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ permutations'Aux t (a :: ts) = (permutationsAux2 t [] [a :: ts ++ [t]] (a :: ts) id).snd

Tactic:
simp only [permutations'Aux, ih, cons_append, permutationsAux2_snd_cons, append_nil, id_eq,
    cons.injEq, true_and]

Goal state after:
case cons
α : Type u_1
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ map (cons a) (permutationsAux2 t [] [ts ++ [t]] ts id).snd =
    (permutationsAux2 t [] [a :: (ts ++ [t])] ts fun x ↦ a :: x).snd
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
hx : x = y
hxy : x ∈ [y]
⊢ [y].prev x hxy = [y].getLast ⋯

Tactic:
simp [prev, hx]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
hx : x = y
head✝ : α
tail✝ : List α
hxy : x ∈ y :: head✝ :: tail✝
⊢ (y :: head✝ :: tail✝).prev x hxy = (y :: head✝ :: tail✝).getLast ⋯

Tactic:
simp [prev, hx]

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ ∀ (i : ℕ) (h₁ : i < (pmap l.next l ⋯).length) (h₂ : i < (l.rotate 1).length), (pmap l.next l ⋯)[i] = (l.rotate 1)[i]

Tactic:
· intros
    rw [getElem_pmap, getElem_rotate, next_getElem _ h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l.prev (l.next x hx) ⋯ = x

Tactic:
by
  obtain ⟨n, hn, rfl⟩ := getElem_of_mem hx
  simp only [next_getElem, prev_getElem, h, Nat.mod_add_mod]
  rcases l with - | ⟨hd, tl⟩
  · simp at hn
  · have : (n + 1 + length tl) % (length tl + 1) = n := by
      rw [length_cons] at hn
      rw [add_assoc, add_comm 1, Nat.add_mod_right, Nat.mod_eq_of_lt hn]
    simp only [length_cons, Nat.succ_sub_succ_eq_sub, Nat.sub_zero, this]

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

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

Tactic:
rw [next_getElem _ (h.nodup_iff.mp hn), getElem_eq_getElem_rotate _ n]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n : ℕ
h : l ~r l.rotate n
⊢ (l.rotate n)[(l.length - n % l.length + (k + 1) % l.length) % l.length] =
    (l.rotate n)[((l.length - n % l.length + k) % l.length + 1) % (l.rotate n).length]
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]
  simp_rw [Set.mem_inv_smul_set_iff, Perm.smul_def, swap_apply_def]
  exact ⟨fun h ↦ by simpa [Iff.comm] using h a, by intros; split_ifs <;> simp [*]⟩

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

Goal state before:
pp: case cons.inl.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c
⊢ r c c

Tactic:
exact hs.1 c (Or.inr rfl)

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

Goal state before:
pp: G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x✝ : X
H : Subgroup G
ω : Quotient (orbitRel G X)
q : orbitRel.Quotient ↥H ↑(orbitRel.Quotient.orbit ω)
x : ↑(orbitRel.Quotient.orbit ω)
⊢ ↑x ∈ Quotient.mk (orbitRel G X) ⁻¹' {ω}

Tactic:
simp only [Set.mem_preimage, Set.mem_singleton_iff]
    have hx := x.property
    rwa [orbitRel.Quotient.mem_orbit] at hx

Goal state after:
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
h : (leftRel H) g₁ g₂
⊢ ⟦g₁⁻¹ • x⟧ = ⟦g₂⁻¹ • x⟧

Tactic:
rw [leftRel_eq] at 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 : g₁⁻¹ * g₂ ∈ H
⊢ ⟦g₁⁻¹ • x⟧ = ⟦g₂⁻¹ • x⟧
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ replicate n p ~ (p ^ n).primeFactorsList

Tactic:
apply Nat.primeFactorsList_unique (List.prod_replicate n p)

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ (p_1 : ℕ), p_1 ∈ replicate n p → Prime p_1
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: ⊢ primeFactors 0 = ∅

Tactic:
by
  ext
  simp

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 : Injective ⇑f
⊢ (map f H).index = H.index * f.range.index

Tactic:
by
  rw [H.index_map, f.ker_eq_bot hf, sup_bot_eq]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
f : ι → Subgroup G
⊢ (⨅ i, f i).relIndex ⊤ ≤ ∏ x, (f x).relIndex ⊤

Tactic:
relIndex_iInf_le

Goal state after:
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 ∧ ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ ∃ n, 0 < n ∧ n ≤ H.index ∧ a ^ n ∈ H

Tactic:
rcases this with ⟨n₁, n₂, hlt, hle, he⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ ∃ n, 0 < n ∧ n ≤ H.index ∧ a ^ n ∈ H
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
a b : ZMod 0
⊢ (a * b).val = a.val * b.val % 0

Tactic:
rw [Nat.mod_zero]
    apply Int.natAbs_mul

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ divisors 0 = ∅

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ properDivisors 0 = ∅

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ divisors 1 = {1}

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ divisorsAntidiagonal 0 = ∅

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ (-z).divisors = z.divisors

Tactic:
by
  ext
  simp

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

Goal state before:
pp: case succ.succ
n b : ℕ
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits n) = n

Tactic:
induction n using Nat.strongRecOn with | ind n h => ?_

Goal state after:
case succ.succ.ind
b n : ℕ
h : ∀ m < n, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits n) = n
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
b hd : ℕ
tl : List ℕ
IH : (∀ x ∈ tl, x < b + 2) → ofDigits (b + 2) tl < (b + 2) ^ tl.length
hl : ∀ x ∈ hd :: tl, x < b + 2
this : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ tl.length * (b + 2)
⊢ hd < b + 2

Tactic:
exact hl hd List.mem_cons_self

Goal state after:
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
⊢ multiplicity a b = multiplicity c d

Tactic:
by
  unfold multiplicity
  rw [h]

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

Goal state before:
pp: case a
b b' : ℕ
h : b' % b = 1
n : ℕ
| n

Tactic:
rw [← ofDigits_digits b' n]

Goal state after:
case a
b b' : ℕ
h : b' % b = 1
n : ℕ
| ofDigits b' (b'.digits n)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case a
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑n

Tactic:
rw [← ofDigits_digits b' n]

Goal state after:
case a
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑(ofDigits b' (b'.digits n))
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
n : ℕ
x : G
⊢ (fun x_1 ↦ x * x_1)^[n] 1 = 1 ↔ x ^ n = 1

Tactic:
mul_left_iterate_apply_one

Goal state after:
G : Type u_1
inst✝ : Monoid G
n : ℕ
x : G
⊢ x ^ n = 1 ↔ x ^ n = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case convert_2
G : Type u_1
inst✝ : Monoid G
x : G
⊢ x ^ minimalPeriod (fun x_1 ↦ x * x_1) 1 = (fun x_1 ↦ x * x_1)^[minimalPeriod (fun x_1 ↦ x * x_1) 1] 1

Tactic:
mul_left_iterate_apply_one

Goal state after:
case convert_2
G : Type u_1
inst✝ : Monoid G
x : G
⊢ x ^ minimalPeriod (fun x_1 ↦ x * x_1) 1 = x ^ minimalPeriod (fun x_1 ↦ x * x_1) 1
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
⊢ ↑(multiplicity p b + 1) ≤ emultiplicity p a

Tactic:
exact Order.add_one_le_of_lt h

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

Goal state before:
pp: b : ℕ
hb : 1 < b
⊢ fixedLengthDigits hb 1 = Finset.image (fun x ↦ [x]) (Finset.range b)

Tactic:
ext
  rw [mem_fixedLengthDigits_iff, List.length_eq_one_iff]
  grind

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ (fixedLengthDigits hb l).card = b ^ l

Tactic:
rw [Set.BijOn.finsetCard_eq (ofDigits b) (bijOn_ofDigits' hb l), Finset.card_range]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

Tactic:
by
  rcases lt_trichotomy (emultiplicity p a) (emultiplicity p b) with (hab | _ | hab)
  · rw [add_comm, emultiplicity_add_of_gt hab, min_eq_left]
    exact le_of_lt hab
  · contradiction
  · rw [emultiplicity_add_of_gt hab, min_eq_right]
    exact le_of_lt hab

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

Goal state before:
pp: f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
⊢ (∏ a ∈ f.support, a ^ f a).factorization = f

Tactic:
factorization_prod (pow_ne_zero _ <| hf · · |>.ne_zero),

Goal state after:
f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
⊢ ∑ x ∈ f.support, (x ^ f x).factorization = f
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: α : Type u_1
p : ℕ
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ (S.prod g).factorization p = ∑ x ∈ S, (g x).factorization p

Tactic:
by
  rw [factorization_prod hS, finsetSum_apply]

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

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ (p * (n + 1))!.factorization p = (p * n)!.factorization p + (n + 1).factorization p + 1

Tactic:
have h0 : 2 ≤ p := hp.two_le

Goal state after:
n p : ℕ
hp : Prime p
h0 : 2 ≤ 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: 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:
Nat.mul_div_cancel_left m (pow_pos hp.pos k),

Goal state after:
k p : ℕ
hp : Prime p
m : ℕ
⊢ m / p ^ m.factorization p = p ^ k * m / p ^ (p ^ k * m).factorization p
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case neg
p n k : ℕ
h : n < p
hnk : k ≤ n
⊢ (n.choose k).factorization p = 0

Tactic:
rw [choose_eq_factorial_div_factorial hnk,
    factorization_div (factorial_mul_factorial_dvd_factorial hnk), Finsupp.coe_tsub,
    Pi.sub_apply, factorization_factorial_eq_zero_of_lt h, zero_tsub]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
h : m + k ≡ m [MOD orderOf x]
⊢ x ^ (m + k) = x ^ m

Tactic:
have hk : x ^ k = 1 := by
      apply pow_eq_one_iff_modEq.2
      exact Nat.ModEq.add_left_cancel' m (by simpa using h)

Goal state after:
case mpr
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
h : m + k ≡ m [MOD orderOf x]
hk : x ^ k = 1
⊢ x ^ (m + k) = x ^ m
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: n p : ℕ
hp : Prime p
hp' : _root_.Prime p
⊢ emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1

Tactic:
have h0 : 2 ≤ p := hp.two_le

Goal state after:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
⊢ emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ card G = card ((G ⧸ zpowers x) × ↥(zpowers x))

Tactic:
← Fintype.card_congr groupEquivQuotientProdSubgroup

Goal state after:
case h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ card G = card G
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
⊢ (C a * p).divX = C a * p.divX

Tactic:
by
  ext
  simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < p✝.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
p : R[X]
x✝ : p ≠ 0
ih : 0 < p.degree → P p
h0' : 0 < (p * X).degree
h0 : ¬0 < p.degree
⊢ P (p * X)

Tactic:
rw [eq_C_of_degree_le_zero (le_of_not_gt h0)] at h0' ⊢

Goal state after:
R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < p✝.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
p : R[X]
x✝ : p ≠ 0
ih : 0 < p.degree → P p
h0' : 0 < (C (p.coeff 0) * X).degree
h0 : ¬0 < p.degree
⊢ P (C (p.coeff 0) * X)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: 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
hb3 : p * b = n
⊢ b = n / p

Tactic:
rw [← hb3, Nat.mul_div_cancel_left b hp]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ ↑p.natDegree = ↑(p.natDegree - q.natDegree + q.natDegree)

Tactic:
tsub_add_cancel_of_le hlt

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ ↑p.natDegree = ↑p.natDegree
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
⊢ Algebra.IsAlgebraic R A ↔ ⊤.IsAlgebraic

Tactic:
delta Subalgebra.IsAlgebraic
  simp only [Algebra.isAlgebraic_def, Algebra.mem_top, forall_prop_of_true]

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

Goal state before:
pp: case inr.refine_1
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✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i

Tactic:
rw [coeff_divByMonic_X_sub_C_rec, ih, eq_comm, Icc_eq_cons_Ioc (Nat.succ_le_iff.mpr hn),
          sum_cons, Nat.sub_self, pow_zero, one_mul, mul_sum]

Goal state after:
case inr.refine_1
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✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ p.coeff n.succ + ∑ x ∈ Ioc n.succ p.natDegree, a ^ (x - (n + 1)) * p.coeff x =
    p.coeff (n + 1) + ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a * (a ^ (i - (n + 1 + 1)) * p.coeff i)