mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.coeff (f.natDegree - 1) ≠ 0

Tactic:
rwa [eraseLead_coeff_of_ne _ (tsub_lt_self _ _).ne, ← nextCoeff_of_natDegree_pos]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < 1
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case hC
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
f : R[X] →+* MvPolynomial σ R := ⋯
g : MvPolynomial σ R →+* R[X] := ⋯
⊢ (f.comp g).comp C = C

pp: case hX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
f : R[X] →+* MvPolynomial σ R := ⋯
g : MvPolynomial σ R →+* R[X] := ⋯
⊢ ∀ (n : σ), (f.comp g) (X n) = X n

Tactic:
· ext a
      dsimp [f, g]
      rw [eval₂_C, Polynomial.eval₂_C]

Goal state after:
case hX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
f : R[X] →+* MvPolynomial σ R := ⋯
g : MvPolynomial σ R →+* R[X] := ⋯
⊢ ∀ (n : σ), (f.comp g) (X n) = X n
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
⊢ ∀ (r : R), r ≠ 0 → n ≤ N → eval₂ i (⅟x) (reflect N (C r * X ^ n)) * x ^ N = eval₂ i x (C r * X ^ n)

Tactic:
r

Goal state after:
case refine_2
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
⊢ r ≠ 0 → n ≤ N → eval₂ i (⅟x) (reflect N (C r * X ^ n)) * x ^ N = eval₂ i x (C r * X ^ n)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p : K[X]
⊢ Irreducible (p * C p.leadingCoeff⁻¹) ↔ Irreducible p

Tactic:
by_cases hp0 : p = 0
  · simp [hp0]
  exact irreducible_mul_isUnit
    (isUnit_C.mpr (IsUnit.mk0 _ (inv_ne_zero (leadingCoeff_ne_zero.mpr hp0))))

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h0 : ¬0 = 1
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
simp [Monic.def.1 hp, Monic.def.1 hq, Ne.symm h0]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
n : ℕ
⊢ ∀ (r : R), r ≠ 0 → n ≤ p.natDegree → (φ (C r * X ^ n)).natDegree = fu (C r * X ^ n).natDegree

Tactic:
r

Goal state after:
case refine_1
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
n : ℕ
r : R
⊢ r ≠ 0 → n ≤ p.natDegree → (φ (C r * X ^ n)).natDegree = fu (C r * X ^ n).natDegree
Module: Mathlib.Algebra.Polynomial.Monic

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

Tactic:
by
  induction n with
  | zero => rw [pow_zero, zero_smul, ← map_one (f := C), nextCoeff_C_eq_zero]
  | succ n ih => rw [pow_succ, (hp.pow n).nextCoeff_mul hp, ih, succ_nsmul]

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

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

Tactic:
rw [commute_X_pow p, reverse_mul_X_pow]

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : MonicDegreeEq R n
⊢ (↑p).coeff n ≠ 0

Tactic:
simp [p.2.1]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
⊢ ((finSuccEquiv R n) f).natDegree = degreeOf 0 f

Tactic:
by_cases c : f = 0

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : f = 0
⊢ ((finSuccEquiv R n) f).natDegree = degreeOf 0 f

case neg
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
⊢ ((finSuccEquiv R n) f).natDegree = degreeOf 0 f
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝ : CommRing R
t : Multiset R
⊢ (Multiset.map (fun i ↦ (X - C i).nextCoeff) t).sum = -t.sum

Tactic:
simp only [nextCoeff_X_sub_C]

Goal state after:
R : Type u
inst✝ : CommRing R
t : Multiset R
⊢ (Multiset.map (fun x ↦ -x) t).sum = -t.sum
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
n : ℕ
⊢ (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n

Tactic:
have := (Commute.one_right x).geom_sum₂_mul_add n

Goal state after:
R : Type u_1
inst✝ : Semiring R
x : R
n : ℕ
this : (∑ i ∈ range n, (x + 1) ^ i * 1 ^ (n - 1 - i)) * x + 1 ^ n = (x + 1) ^ n
⊢ (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case left
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q : R[X]
⊢ ∀ ⦃a₂ : R[X]⦄, (fun x ↦ p * x) q = (fun x ↦ p * x) a₂ → q = a₂

Tactic:
r

Goal state after:
case left
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
⊢ (fun x ↦ p * x) q = (fun x ↦ p * x) r → q = r
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q : R[X]
⊢ ∀ ⦃a₂ : R[X]⦄, (fun x ↦ x * p) q = (fun x ↦ x * p) a₂ → q = a₂

Tactic:
r

Goal state after:
case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
⊢ (fun x ↦ x * p) q = (fun x ↦ x * p) r → q = r
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : x = 0
⊢ x ∈ degreeLT R (n + 1) ↔ x ∈ degreeLE R ↑n

pp: case neg
R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
⊢ x ∈ degreeLT R (n + 1) ↔ x ∈ degreeLE R ↑n

Tactic:
· simp_rw [x_zero, Submodule.zero_mem]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
⊢ x ∈ degreeLT R (n + 1) ↔ x ∈ degreeLE R ↑n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
x : R
⊢ x ∈ I.leadingCoeffNth n ↔ ∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x

Tactic:
simp only [leadingCoeffNth, degreeLE, Submodule.mem_map, lcoeff_apply, Submodule.mem_inf,
    mem_degreeLE]
  constructor
  · rintro ⟨p, ⟨hpdeg, hpI⟩, rfl⟩
    rcases lt_or_eq_of_le hpdeg with hpdeg | hpdeg
    · refine ⟨0, I.zero_mem, bot_le, ?_⟩
      rw [leadingCoeff_zero, eq_comm]
      exact coeff_eq_zero_of_degree_lt hpdeg
    · refine ⟨p, hpI, le_of_eq hpdeg, ?_⟩
      rw [Polynomial.leadingCoeff, natDegree, hpdeg, Nat.cast_withBot, WithBot.unbotD_coe]
  · rintro ⟨p, hpI, hpdeg, rfl⟩
    have : natDegree p + (n - natDegree p) = n :=
      add_tsub_cancel_of_le (natDegree_le_of_degree_le hpdeg)
    refine ⟨p * X ^ (n - natDegree p), ⟨?_, I.mul_mem_right _ hpI⟩, ?_⟩
    · apply le_trans (degree_mul_le _ _) _
      apply le_trans (add_le_add degree_le_natDegree (degree_X_pow_le _)) _
      rw [← Nat.cast_add, this]
    · rw [Polynomial.leadingCoeff, ← coeff_mul_X_pow p (n - natDegree p), this]

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
⊢ IsNoetherianRing S

Tactic:
by
  obtain ⟨s, hs⟩ := h.1
  apply
    isNoetherianRing_of_surjective (MvPolynomial s R) S
      (MvPolynomial.aeval (↑) : MvPolynomial s R →ₐ[R] S).toRingHom
  rw [← Set.range_eq_univ, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, ← AlgHom.coe_range,
    ← Algebra.adjoin_range_eq_range_aeval, Subtype.range_coe_subtype, Finset.setOfPred_mem, hs]
  rfl

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
t : Set A
h : t.Finite
⊢ FiniteType R ↥(adjoin R t)

Tactic:
rw [← Subalgebra.fg_iff_finiteType]
  exact ⟨h.toFinset, by simp⟩

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
this : of' R M '' ⋃ f ∈ S, ↑f.coeff.support = ⋃ f ∈ S, of' R M '' ↑f.coeff.support
⊢ adjoin R (of' R M '' ⋃ f ∈ S, ↑f.coeff.support) = ⊤

Tactic:
by
    rw [this]
    exact support_gen_of_gen hS

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set R[M]
hS : adjoin R S = ⊤
this : ⇑(of R M) '' ⋃ f ∈ S, ↑f.coeff.support = ⋃ f ∈ S, ⇑(of R M) '' ↑f.coeff.support
⊢ adjoin R (⇑(of R M) '' ⋃ f ∈ S, ↑f.coeff.support) = ⊤

Tactic:
by
    rw [this]
    exact support_gen_of_gen hS

Goal state after:
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
⊢ n = 0

Tactic:
obtain ⟨k, mj, hmj⟩ := exists_fin (R := R) (M := M)

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 : span R (Set.range mj) = ⊤
⊢ n = 0
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
⊢ ker (Ideal.Quotient.lift I f H) = ⊥

Tactic:
RingHom.ker_eq_bot_iff_eq_zero

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
⊢ ∀ (x : R ⧸ I), (Ideal.Quotient.lift I f H) x = 0 → x = 0
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
S : Type v
F : Type w
inst✝⁹ : Ring R
inst✝⁸ : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : Ring A
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
inst✝² : Semiring B
inst✝¹ : Algebra R₁ B
I : Ideal A
inst✝ : I.IsTwoSided
f : A →ₐ[R₁] B
hI : ∀ a ∈ I, f a = 0
r : R₁
this : (algebraMap R₁ (A ⧸ I)) r = (mk I) ((algebraMap R₁ A) r)
⊢ ↑f ((algebraMap R₁ A) r) = (algebraMap R₁ B) r

Tactic:
AlgHom.coe_toRingHom,

Goal state after:
R : Type u
S : Type v
F : Type w
inst✝⁹ : Ring R
inst✝⁸ : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : Ring A
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
inst✝² : Semiring B
inst✝¹ : Algebra R₁ B
I : Ideal A
inst✝ : I.IsTwoSided
f : A →ₐ[R₁] B
hI : ∀ a ∈ I, f a = 0
r : R₁
this : (algebraMap R₁ (A ⧸ I)) r = (mk I) ((algebraMap R₁ A) r)
⊢ f ((algebraMap R₁ A) r) = (algebraMap R₁ B) r
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m : ℕ
hm : m < minimalPeriod f x
n : ℕ
hn : n < minimalPeriod f x
hmn : f^[m] x = f^[n] x
⊢ m = n

Tactic:
rwa [iterate_eq_iterate_iff_of_lt_minimalPeriod hm hn] at hmn

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d d' : α
x_mem : x ∈ xs.dropLast
⊢ xs.nextOr x d = xs.nextOr x d'

Tactic:
induction xs with

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x d d' y : α
ys : List α
IH : x ∈ ys.dropLast → ys.nextOr x d = ys.nextOr x d'
x_mem : x ∈ (y :: ys).dropLast
⊢ (y :: ys).nextOr x d = (y :: ys).nextOr x d'
Module: Mathlib.Data.List.Cycle

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

Tactic:
induction xs with

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x d y : α
ys : List α
IH : ys.nextOr x d ≠ d → x ∈ ys
h : (y :: ys).nextOr x d ≠ d
⊢ x ∈ y :: ys
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (z :: zs).nextOr x d ≠ d
hx : ¬x = y
⊢ x ∈ y :: z :: zs

Tactic:
simpa [hx] using IH h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
h : x ∉ xs
⊢ (xs ++ [x]).nextOr x d = d

Tactic:
induction xs with

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
xs' : List α
hxs' : ∀ x ∈ xs, x ∈ xs'
hd : d ∈ xs'
⊢ xs.nextOr x d ∈ xs'

Tactic:
induction xs with

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y : α
ys : List α
ih : (∀ x ∈ ys, x ∈ xs') → ys.nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: ys, x ∈ xs'
⊢ (y :: ys).nextOr x d ∈ xs'
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
x : α
⊢ count [x] (permutations'Aux x []) = (takeWhile (fun x_1 ↦ decide (x = x_1)) []).length + 1

Tactic:
simp [takeWhile, count]

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

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

Tactic:
by cases l <;> simp [prev, hx]

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

Goal state before:
pp: α : Type u_1
s : List α
hs : s.Nodup
⊢ s.permutations.Nodup

Tactic:
(permutations_perm_permutations' s).nodup_iff

Goal state after:
α : Type u_1
s : List α
hs : s.Nodup
⊢ s.permutations'.Nodup
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ l.reverse.prev l[k] ⋯ = (pmap l.next l ⋯)[k]

Tactic:
getElem_eq_getElem_reverse (l := l),

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ l.reverse.prev l.reverse[l.length - 1 - k] ⋯ = (pmap l.next l ⋯)[k]
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
x : α
hx : x ∈ l
⊢ l.reverse.next x ⋯ = l'.reverse.next x ⋯

Tactic:
exact isRotated_next_eq h.reverse (nodup_reverse.mpr hn) _

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
h : G
⊢ g⁻¹ * h * g ∈ stabilizer G a ↔ h ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (stabilizer G a)

Tactic:
Subgroup.mem_map_equiv,

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
h : G
⊢ g⁻¹ * h * g ∈ stabilizer G a ↔ (MulEquiv.symm (MulAut.conj g)) h ∈ stabilizer G a
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
g h k : G
a b c : α
hg : b = g • a
⊢ Subgroup.map (↑(MulAut.conj g)) (stabilizer G a) = stabilizer G b

Tactic:
hg,

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
g h k : G
a b c : α
hg : b = g • a
⊢ Subgroup.map (↑(MulAut.conj g)) (stabilizer G a) = stabilizer G (g • a)
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x : M
hx : x ≠ 0
g : Rˣ
hg : ↑g • x = x
⊢ ↑g • x - 1 • x = 0

Tactic:
hg,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x : M
hx : x ≠ 0
g : Rˣ
hg : ↑g • x = x
⊢ x - 1 • x = 0
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
H : Subgroup G
inst✝ : Finite (G ⧸ H)
⊢ Finite (orbitRel.Quotient (↥H) X)

Tactic:
rcases isEmpty_or_nonempty X with he | ⟨⟨b⟩⟩
  · exact Quotient.finite _
  · have h' : Finite (Quotient (rightRel H)) :=
      Finite.of_equiv _ (quotientRightRelEquivQuotientLeftRel _).symm
    let f : Quotient (rightRel H) → orbitRel.Quotient H X :=
      fun a ↦ Quotient.liftOn' a (fun g ↦ ⟦g • b⟧) fun g₁ g₂ r ↦ by
        replace r := Setoid.symm' _ r
        rw [rightRel_eq] at r
        simp only [Quotient.eq, orbitRel_apply, mem_orbit_iff]
        exact ⟨⟨g₁ * g₂⁻¹, r⟩, by simp [mul_smul]⟩
    exact Finite.of_surjective f ((Quotient.surjective_liftOn' _).2
      (Quotient.mk''_surjective.comp (MulAction.surjective_smul _ _)))

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

Goal state before:
pp: case refine_2
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ l → _root_.Prime p

pp: case refine_3
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ n.primeFactorsList → _root_.Prime p

Tactic:
· simp_rw [← prime_iff]
    exact h₂

Goal state after:
case refine_3
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ n.primeFactorsList → _root_.Prime p
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.primeFactorsList.prod = (replicate k p).prod

Tactic:
eq_replicate_of_mem fun d hd =>
    h (prime_of_mem_primeFactorsList hd) (dvd_of_mem_primeFactorsList hd)

Goal state after:
n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
k : ℕ := n.primeFactorsList.length
⊢ (replicate n.primeFactorsList.length p).prod = (replicate k p).prod
Module: Mathlib.Data.Nat.Factors

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

Tactic:
refine (primeFactorsList_unique ?_ ?_).symm

Goal state after:
case refine_1
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.primeFactorsList ++ b.primeFactorsList).prod = a * b

case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ (p : ℕ), p ∈ a.primeFactorsList ++ b.primeFactorsList → Prime p
Module: Mathlib.GroupTheory.Index

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

Tactic:
simp [Subgroup.relIndex, Subgroup.index_eq_two_iff, mem_subgroupOf]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⊥.relIndex H * H.index = ⊥.index

Tactic:
exact relIndex_mul_index bot_le

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

Goal state before:
pp: case zero
a : ℕ
⊢ (↑a).val = a % 0

Tactic:
rw [Nat.mod_zero]

Goal state after:
case zero
a : ℕ
⊢ (↑a).val = a
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
x : X
inst✝ : IsPretransitive G X
⊢ (stabilizer G x).index = Nat.card X

Tactic:
rw [index_stabilizer, orbit_eq_univ, Set.ncard_univ]

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

Goal state after:
case zero
a b : ZMod 0
⊢ (a * b).val = a.val * b.val
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
⊢ p.divisors = {1, p}

Tactic:
ext
  rw [mem_divisors, dvd_prime pp, and_iff_left pp.ne_zero, Finset.mem_insert, Finset.mem_singleton]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f (n / i) i

Tactic:
rw [← map_swap_divisorsAntidiagonal, Finset.prod_map]
  exact prod_divisorsAntidiagonal fun i j => f j i

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

Goal state before:
pp: n : ℕ
⊢ n.divMaxPow 0 = n

Tactic:
simp [divMaxPow]

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

Goal state before:
pp: n : ℕ
⊢ n.divMaxPow 1 = n

Tactic:
simp [divMaxPow]

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

Goal state before:
pp: p : ℕ
⊢ divMaxPow 0 p = 0

Tactic:
simp [divMaxPow]

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

Goal state before:
pp: p : ℕ
⊢ divMaxPow 1 p = 1

Tactic:
simp [divMaxPow]

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

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

Tactic:
rcases eq_or_lt_of_le (Nat.succ_le_of_lt hb) with (rfl | hb)
  · simp
  rw [← ofDigits_digits_append_digits]
  refine (digits_ofDigits b hb _ (fun l hl => ?_) (fun h_append => ?_)).symm
  · rcases (List.mem_append.mp hl) with (h | h) <;> exact digits_lt_base hb h
  · by_cases h : digits b m = []
    · simp only [h, List.append_nil] at h_append ⊢
      exact getLast_digit_ne_zero b <| digits_ne_nil_iff_ne_zero.mp h_append
    · exact (List.getLast_append_of_right_ne_nil _ _ h) ▸
          (getLast_digit_ne_zero _ <| digits_ne_nil_iff_ne_zero.mp h)

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

Goal state before:
pp: b m : ℕ
hm : m ≠ 0
this : (b + 2).digits m ≠ []
⊢ (b + 2) ^ ((b + 2).digits m).length ≤ (b + 2) * m

Tactic:
convert! @pow_length_le_mul_ofDigits b (digits (b + 2) m) this (getLast_digit_ne_zero _ hm)

Goal state after:
b m : ℕ
hm : m ≠ 0
this : (b + 2).digits m ≠ []
⊢ m = ofDigits (b + 2) ((b + 2).digits m)