mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: case pos
n : ℕ
M : Type u_1
inst✝ : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
c_a : a = 0
⊢ (cons (t 0) t.tail) a = t a

Tactic:
c_a,

Goal state after:
case pos
n : ℕ
M : Type u_1
inst✝ : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
c_a : a = 0
⊢ (cons (t 0) t.tail) 0 = t 0
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
⊢ cons 0 (single i y) = single i.succ y

Tactic:
by
  ext j
  cases j using Fin.cases <;> simp [single_apply]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
⊢ ∑ x ∈ φ.support, (eval₂Hom f g) ((monomial x) (coeff x φ)) = 0

Tactic:
refine Finset.sum_eq_zero fun d hd => ?_

Goal state after:
R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (eval₂Hom f g) ((monomial d) (coeff d φ)) = 0
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
d : σ →₀ ℕ
hd : d ∈ φ.support
i : σ
hi : i ∈ d.support
hgi : g i = 0
⊢ g i ^ d i = 0

Tactic:
rw [hgi, zero_pow]

Goal state after:
R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
d : σ →₀ ℕ
hd : d ∈ φ.support
i : σ
hi : i ∈ d.support
hgi : g i = 0
⊢ d i ≠ 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: N a b : ℕ
hab : revAtFun N a = revAtFun N b
⊢ revAtFun N (revAtFun N a) = b

Tactic:
hab,

Goal state after:
N a b : ℕ
hab : revAtFun N a = revAtFun N b
⊢ revAtFun N (revAtFun N b) = b
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree = 0
⊢ (map f p).natDegree = 0

Tactic:
← Nat.le_zero,

Goal state after:
case inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree = 0
⊢ (map f p).natDegree ≤ 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ (p.comp (-X)).leadingCoeff = (-1) ^ p.natDegree * p.leadingCoeff

Tactic:
by
  nontriviality R
  by_cases h : p = 0
  · simp [h]
  rw [Polynomial.leadingCoeff, natDegree_comp_eq_of_mul_ne_zero, coeff_comp_degree_mul_degree] <;>
  simp [((Commute.neg_one_left _).pow_left _).eq, h]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
j : Option S₁ →₀ ℕ
r : R
n : Option S₁ →₀ ℕ
hj : ¬j = n
⊢ if j = n then (if j none = n none then if j.some = n.some then r else 0 else 0) = r
  else (if j none = n none then if j.some = n.some then r else 0 else 0) = 0

Tactic:
· rw [if_neg hj]
      simp only [ite_eq_right_iff]
      intro hj_none hj_some
      apply False.elim (hj _)
      simp only [Finsupp.ext_iff, Option.forall, hj_none, true_and]
      simpa only [Finsupp.ext_iff] using! hj_some

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.reverse.natDegree + f.natTrailingDegree ≤ f.natDegree

Tactic:
← le_tsub_iff_left f.reverse_natDegree_le

Goal state after:
case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natTrailingDegree ≤ f.natDegree - f.reverse.natDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
ih : (p ^ n).nextCoeff = n • p.nextCoeff
⊢ (p ^ (n + 1)).nextCoeff = (n + 1) • p.nextCoeff

Tactic:
| succ n ih =>

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : (p * X ^ n).reverse = p.reverse
⊢ (p * X ^ (n + 1)).reverse = p.reverse

Tactic:
| succ n ih =>

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) ^ (n + 1)

Tactic:
| succ n ih =>

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

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ ↑(image (fun n ↦ X ^ n) (range (n + 1))) ⊆ ↑(degreeLE R ↑n)

Tactic:
Finset.coe_image,

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ (fun n ↦ X ^ n) '' ↑(range (n + 1)) ⊆ ↑(degreeLE R ↑n)
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q = 0 → q * p = 0

Tactic:
rintro rfl
    rw [zero_mul]

Goal state after:
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_1.refine_1
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ x ∈ adjoin R (s ∪ t)

Tactic:
have : x ∈ Subalgebra.toSubmodule (adjoin R s) := by
        rw [← hp']
        exact subset_span hx
      exact adjoin_mono Set.subset_union_left this

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

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ ↑(image (fun n ↦ X ^ n) (range n)) ⊆ ↑(degreeLT R n)

Tactic:
Finset.coe_image,

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ (fun n ↦ X ^ n) '' ↑(range n) ⊆ ↑(degreeLT R n)
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
s : Finset S
hs : adjoin R ↑s = ⊤
t : Finset A
ht : adjoin S ↑t = ⊤
⊢ adjoin R (↑(Finset.image (⇑(algebraMap S A)) s) ∪ ↑t) = ⊤

Tactic:
Finset.coe_image,

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
s : Finset S
hs : adjoin R ↑s = ⊤
t : Finset A
ht : adjoin S ↑t = ⊤
⊢ adjoin R (⇑(algebraMap S A) '' ↑s ∪ ↑t) = ⊤
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
n : ℕ
ih : ∀ (i : ℕ), ((∑ i ∈ range n, X ^ i).comp (X + 1)).coeff i = ↑(n.choose (i + 1))
i : ℕ
⊢ ((∑ i ∈ range (n + 1), X ^ i).comp (X + 1)).coeff i = ↑((n + 1).choose (i + 1))

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs✝ : S.FG
s : Finset A
hs : Algebra.adjoin R ↑s = S
⊢ Algebra.adjoin R ↑(Finset.image (⇑f) s) = Subalgebra.map f S

Tactic:
Finset.coe_image,

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs✝ : S.FG
s : Finset A
hs : Algebra.adjoin R ↑s = S
⊢ Algebra.adjoin R (⇑f '' ↑s) = Subalgebra.map f S
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case intro
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
val✝ : Fintype ι
⊢ adjoin S ↑(Finset.image MvPolynomial.X Finset.univ) = ⊤

Tactic:
Finset.coe_image,

Goal state after:
case intro
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
val✝ : Fintype ι
⊢ adjoin S (MvPolynomial.X '' ↑Finset.univ) = ⊤
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
⊢ FiniteType R (MvPolynomial ι S)

Tactic:
by
  classical
  cases nonempty_fintype ι
  refine .trans ‹_› ⟨Finset.univ.image MvPolynomial.X, ?_⟩
  rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
  exact MvPolynomial.adjoin_range_X

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case intro
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
val✝ : Fintype ι
⊢ adjoin S ↑(Finset.image (FreeAlgebra.ι S) Finset.univ) = ⊤

Tactic:
Finset.coe_image,

Goal state after:
case intro
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
val✝ : Fintype ι
⊢ adjoin S (FreeAlgebra.ι S '' ↑Finset.univ) = ⊤
Module: Mathlib.GroupTheory.GroupAction.Ring

Goal state before:
pp: case succ
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : R
n : ℕ
ih : (n • x) • y = n • x • y
⊢ ((n + 1) • x) • y = (n + 1) • x • y

Tactic:
| succ n ih =>

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

Goal state before:
pp: n a b c : ℤ
⊢ n * b + a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

Tactic:
rw [add_comm, add_modulus_mul_modEq_iff]

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
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
u : R ⧸ I
⊢ (Ideal.Quotient.lift I f H) u = 0 → u = 0

Tactic:
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
u : R ⧸ I
hu : (Ideal.Quotient.lift I f H) u = 0
⊢ u = 0
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Surjective ⇑f
g : A →ₐ[R] C
H : ker f.toRingHom ≤ ker g.toRingHom
x : A
⊢ (f.liftOfSurjective hf g H) (f x) = g x

Tactic:
dsimp [AlgHom.liftOfSurjective]
  erw [AlgEquiv.coe_toAlgHom] -- fixed after #21031
  rw [Ideal.quotientKerAlgEquivOfSurjective_symm_apply]
  rfl

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Fintype α
l : List α
⊢ (l ∈
      let univSubsets := Finset.univ.powerset.val;
      let allPerms := univSubsets.bind fun s ↦ s.val.lists;
      { val := allPerms, nodup := ⋯ }) ↔
    l.Nodup

Tactic:
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]

Goal state after:
case refine_2
α : Type u_1
inst✝ : Fintype α
l : List α
⊢ (∃ a, a.val = ↑l) ↔ l.Nodup
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case refine_4
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ Function.Surjective fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩

Tactic:
· intro ⟨x, hx⟩
    rw [Ideal.mem_map_iff_of_surjective _ Ideal.Quotient.mk_surjective] at hx
    obtain ⟨y, hy, rfl⟩ := hx
    refine ⟨Submodule.Quotient.mk ⟨y, hy⟩, ?_⟩
    simp

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

Goal state before:
pp: α : Type u_1
is ts : List α
⊢ (is ++ ts).permutations = map (fun x ↦ x ++ ts) is.permutations ++ ts.permutationsAux is.reverse

Tactic:
by
  simp [permutations, permutationsAux_append]

Goal state after:
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

Tactic:
← Nat.mod_add_div n (period m a),

Goal state after:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
| m ^ (n % period m a + period m a * (n / period m a)) • a
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case succ.refine_1
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts : List α
h : ts.length < n + 1
x✝ : [].length < n + 1
⊢ [].permutations ~ [].permutations'

Tactic:
simp [permutations]

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

Goal state before:
pp: case inr
α : Type u_1
f : α → α
inst✝ : Finite α
h : Injective f
x : α
m n : ℕ
heq : f^[m] x = f^[n] x
hne : m ≠ n
hlt : n < m
⊢ x ∈ periodicPts f

Tactic:
· exact mk_mem_periodicPts (by lia) (iterate_cancel h heq)

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

Goal state before:
pp: case cons
α : Type u_1
x y : α
s : List α
IH : ¬x ∈ s → (permutations'Aux x s).Nodup
hx : ¬x ∈ y :: s
⊢ (permutations'Aux x (y :: s)).Nodup

Tactic:
simp only [not_or, mem_cons] at hx

Goal state after:
case cons
α : Type u_1
x y : α
s : List α
IH : ¬x ∈ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
⊢ (permutations'Aux x (y :: s)).Nodup
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case nil
α : Type u_1
x y : α
⊢ take 2 [x, y].permutations = [[x, y], [y, x]]

Tactic:
simp [permutations]

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

Goal state before:
pp: case cons
α : Type u_1
x y head✝ : α
tail✝ : List α
tail_ih✝ : take 2 (x :: y :: tail✝).permutations = [x :: y :: tail✝, y :: x :: tail✝]
⊢ take 2 (x :: y :: head✝ :: tail✝).permutations = [x :: y :: head✝ :: tail✝, y :: x :: head✝ :: tail✝]

Tactic:
simp [permutations]

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

Goal state before:
pp: M : Type u
inst✝² : Monoid M
α : Type v
inst✝¹ : MulAction M α
β : Type u_1
inst✝ : MulAction M β
x y : α × β
h : x ∈ orbit M y
⊢ x.1 ∈ orbit M y.1

Tactic:
by
  rcases h with ⟨g, rfl⟩
  exact mem_orbit _ _

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

Goal state before:
pp: M : Type u
inst✝² : Monoid M
α : Type v
inst✝¹ : MulAction M α
β : Type u_1
inst✝ : MulAction M β
x y : α × β
h : x ∈ orbit M y
⊢ x.2 ∈ orbit M y.2

Tactic:
by
  rcases h with ⟨g, rfl⟩
  exact mem_orbit _ _

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
⊢ a ∣ (a :: l₁).prod

Tactic:
by rw [prod_cons]; exact dvd_mul_right _ _

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

Goal state before:
pp: G : Type u
X : Type v
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : H.Normal
inst✝² : SMul G X
inst✝¹ : MulAction (G ⧸ H) X
inst✝ : IsScalarTower G (G ⧸ H) X
g : G
x : X
⊢ ↑g • x = (g • 1) • x

Tactic:
← QuotientGroup.mk_one,

Goal state after:
G : Type u
X : Type v
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : H.Normal
inst✝² : SMul G X
inst✝¹ : MulAction (G ⧸ H) X
inst✝ : IsScalarTower G (G ⧸ H) X
g : G
x : X
⊢ ↑g • x = (g • ↑1) • x
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ p.primeFactorsList = [p]

Tactic:
rw [this, primeFactorsList]

Goal state after:
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ (p - 2 + 2).minFac :: ((p - 2 + 2) / (p - 2 + 2).minFac).primeFactorsList = [p - 2 + 2]
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: n p : ℕ
⊢ p ∈ n.primeFactors ↔ Prime p ∧ p ∣ n ∧ n ≠ 0

Tactic:
simp_rw [← toFinset_factors, List.mem_toFinset, mem_primeFactorsList']

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

Goal state before:
pp: case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ (MulAction.toPermHom G (G ⧸ H)).ker
⊢ ↑(g * 1) = ↑1

Tactic:
exact (MulAction.Quotient.smul_mk H g 1).symm.trans (Equiv.Perm.ext_iff.mp hg (1 : G))

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

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

Tactic:
| succ n ih =>

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

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ ↑(1 % (n✝ + 1 + 1)) = 1

Tactic:
rw [Nat.mod_eq_of_lt]

Goal state after:
case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ ↑1 = 1

case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ 1 < n✝ + 1 + 1
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hlt : 0 < n
hle : n ≤ (H.subgroupOf K).index
he : ⟨a, ha⟩ ^ n ∈ H.subgroupOf K
⊢ ∃ n, 0 < n ∧ n ≤ H.relIndex K ∧ a ^ n ∈ H ⊓ K

Tactic:
refine ⟨n, hlt, hle, ?_⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hlt : 0 < n
hle : n ≤ (H.subgroupOf K).index
he : ⟨a, ha⟩ ^ n ∈ H.subgroupOf K
⊢ a ^ n ∈ H ⊓ K
Module: Mathlib.Algebra.Algebra.ZMod

Goal state before:
pp: case zero
R✝ : Type u_1
inst✝¹ : Ring R✝
R : Type u_2
inst✝ : Ring R
x : R
r : ZMod 0
⊢ r • 1 * x = r • x ∧ x * r • 1 = r • x

Tactic:
simp [ZMod, Int.cast_comm]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
ih : if Even n then ∑ i ∈ range n, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range n, x ^ i
⊢ if Even (n + 1) then ∑ i ∈ range (n + 1), x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range (n + 1), x ^ i

Tactic:
| succ n ih =>

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

Goal state before:
pp: n : ℕ
a : ZMod n
⊢ a * a⁻¹ = ↑(a.val.gcd n)

Tactic:
rcases n with - | n
  · dsimp [ZMod] at a ⊢
    calc
      _ = a * Int.sign a := rfl
      _ = a.natAbs := by rw [Int.mul_sign_self]
      _ = a.natAbs.gcd 0 := by rw [Nat.gcd_zero_right]
  · calc
      a * a⁻¹ = a * a⁻¹ + n.succ * Nat.gcdB (val a) n.succ := by
        rw [natCast_self, zero_mul, add_zero]
      _ = ↑(↑a.val * Nat.gcdA (val a) n.succ + n.succ * Nat.gcdB (val a) n.succ) := by
        push_cast
        rw [natCast_zmod_val]
        rfl
      _ = Nat.gcd a.val n.succ := by rw [← Nat.gcd_eq_gcd_ab a.val n.succ]; rfl

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

Goal state before:
pp: case succ
n : ℕ
u : (ZMod (n + 1))ˣ
this : ↑(u * u⁻¹) = 1
⊢ (↑u).val * (↑u⁻¹).val ≡ 1 [MOD n + 1]

Tactic:
rw [← natCast_eq_natCast_iff, Nat.cast_one, ← this]

Goal state after:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
this : ↑(u * u⁻¹) = 1
⊢ ↑((↑u).val * (↑u⁻¹).val) = ↑(u * u⁻¹)
Module: Mathlib.Data.Nat.Digits.Defs

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

Tactic:
| succ n ih =>

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

Goal state before:
pp: p k a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
⊢ p ^ k ∣ p ^ a * b ↔ k ≤ a

Tactic:
cases Nat.lt_or_ge a k with
  | inl hlt =>
    refine iff_of_false (fun hdvd ↦ ?_) (Nat.not_le_of_lt hlt)
    obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_lt hlt
    rw [Nat.add_assoc, Nat.pow_add,
      Nat.mul_dvd_mul_iff_left (Nat.pow_pos (Nat.zero_lt_of_lt hp))] at hdvd
    exact hb <| Nat.dvd_of_pow_dvd (Nat.le_add_left 1 l) hdvd
  | inr hle =>
    refine iff_of_true (Nat.dvd_mul_right_of_dvd ?_ _) hle
    exact Nat.pow_dvd_pow p hle

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

Goal state before:
pp: case succ.cons.hbc
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ p ≤ p * p ^ i - p * (ofDigits p tl % p ^ i)

Tactic:
· rw [← Nat.mul_sub]
        exact Nat.le_mul_of_pos_right _ <| Nat.sub_pos_of_lt <| mod_lt _ <| pow_pos hpos i

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

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

Tactic:
refine Finset.induction_on' S ?_ ?_

Goal state after:
case refine_1
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ (∅.prod g).factorization = ∑ x ∈ ∅, (g x).factorization

case refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ ∀ (a : α) (s : Finset α),
    a ∈ S →
      s ⊆ S →
        a ∉ s →
          (s.prod g).factorization = ∑ x ∈ s, (g x).factorization →
            ((insert a s).prod g).factorization = ∑ x ∈ insert a s, (g x).factorization
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n r : ℕ
hx : x ^ (2 * r + 1) = 1
⊢ x ^ (2 * (r + 1)) = x

Tactic:
have h2 : 2 * (r + 1) = 2 * r + 1 + 1 := by omega

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n r : ℕ
hx : x ^ (2 * r + 1) = 1
h2 : 2 * (r + 1) = 2 * r + 1 + 1
⊢ x ^ (2 * (r + 1)) = x
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), m.factorization p = 0
⊢ ∑ i ∈ Ico 1 (p * n + 1), i.factorization p + (1 + (n + 1).factorization p) =
    ∑ x ∈ Ico 1 (p * n + 1), x.factorization p + ((n + 1).factorization p + 1)

Tactic:
add_comm 1

Goal state after:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), m.factorization p = 0
⊢ ∑ i ∈ Ico 1 (p * n + 1), i.factorization p + ((n + 1).factorization p + 1) =
    ∑ x ∈ Ico 1 (p * n + 1), x.factorization p + ((n + 1).factorization p + 1)
Module: Mathlib.Data.Nat.Choose.Factorization

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

Tactic:
| succ n ih =>

Goal state after: