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
⊢ f.eraseLead.natDegree ≤ f.natDegree - 2

Tactic:
by
  refine natDegree_le_pred (n := f.natDegree - 1) (eraseLead_natDegree_le f) ?_
  rw [nextCoeff_eq_zero, natDegree_eq_zero] at h
  obtain ⟨a, rfl⟩ | ⟨hf, h⟩ := h
  · simp
  rw [eraseLead_coeff_of_ne _ (tsub_lt_self hf zero_lt_one).ne, ← nextCoeff_of_natDegree_pos hf]
  simp [nextCoeff_eq_zero, h, eq_zero_or_pos]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case pos.refine_2
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
⊢ b ∈ s → (WithBot.some ∘ fun i ↦ (f i).natDegree) b ≤ s.sup' hs fun i ↦ (f i).degree

Tactic:
hb

Goal state after:
case pos.refine_2
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
⊢ (WithBot.some ∘ fun i ↦ (f i).natDegree) b ≤ s.sup' hs fun i ↦ (f i).degree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
h' : (((optionEquivLeft R σ) f).support.sup fun x ↦ x) = degreeOf none f
⊢ ((optionEquivLeft R σ) f).degree = ↑(degreeOf none f)

Tactic:
rw [Polynomial.degree, ← h', Nat.cast_withBot,
    Finset.coe_sup_of_nonempty (nonempty_support_optionEquivLeft R h), Finset.max_eq_sup_coe,
    Function.comp_def]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

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

Tactic:
degree_mul_leadingCoeff_self_inv

Goal state after:
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
⊢ p.degree = p.degree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case none
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
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (((aevalTower (Polynomial.aeval (X none)) fun i ↦ X (Option.some i)).comp
          (aeval fun o ↦ o.elim (C Polynomial.X) X))
        (X none)) =
    coeff m✝ ((AlgHom.id R (MvPolynomial (Option S₁) R)) (X none))

Tactic:
simp only [Option.elim, AlgHom.coe_comp, comp_apply, aeval_X, aevalTower_C,
          Polynomial.aeval_X, AlgHom.coe_id, id, aevalTower_X]

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

Goal state before:
pp: case some
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
val✝ : S₁
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (((aevalTower (Polynomial.aeval (X none)) fun i ↦ X (Option.some i)).comp
          (aeval fun o ↦ o.elim (C Polynomial.X) X))
        (X (Option.some val✝))) =
    coeff m✝ ((AlgHom.id R (MvPolynomial (Option S₁) R)) (X (Option.some val✝)))

Tactic:
simp only [Option.elim, AlgHom.coe_comp, comp_apply, aeval_X, aevalTower_C,
          Polynomial.aeval_X, AlgHom.coe_id, id, aevalTower_X]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
⊢ p = 1

Tactic:
nontriviality R
  obtain ⟨q, h⟩ := hpu.exists_right_inv
  have := hm.natDegree_mul' (right_ne_zero_of_mul_eq_one h)
  rw [h, natDegree_one, eq_comm, add_eq_zero] at this
  exact hm.natDegree_eq_zero.mp this.1

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

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hg : g.Monic
hp : (f * g).Monic
hp1 : f * g ≠ 1
h : ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 ((f * g).natDegree / 2) → ¬q ∣ f * g
hdg : g.natDegree ∈ Ioc 0 ((f * g).natDegree / 2)
⊢ False

Tactic:
exact h g hg hdg (dvd_mul_left g f)

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

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

Tactic:
by
  have := (Commute.one_right x).geom_sum₂_mul n
  rw [one_pow, geom_sum₂_with_one] at this
  exact this

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
k : ℕ
x✝ : k ∈ Ico m n
⊢ MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k = MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)

Tactic:
have hp := Commute.pow_pow (Commute.op h.symm) (n - 1 - k) k

Goal state after:
R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
k : ℕ
x✝ : k ∈ Ico m n
hp : Commute (MulOpposite.op y ^ (n - 1 - k)) (MulOpposite.op x ^ k)
⊢ MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k = MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
Module: Mathlib.Algebra.Ring.Action.Submonoid

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction M α
a✝ b✝ : α
ha : a✝ ∈ MulAction.fixedPoints M α
hb : b✝ ∈ MulAction.fixedPoints M α
x✝ : M
⊢ a✝ + x✝ • b✝ = a✝ + b✝

Tactic:
hb

Goal state after:
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction M α
a✝ b✝ : α
ha : a✝ ∈ MulAction.fixedPoints M α
hb : b✝ ∈ MulAction.fixedPoints M α
x✝ : M
⊢ a✝ + b✝ = a✝ + b✝
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : S.FG
⊢ (map S.val ⊤).FG

Tactic:
Algebra.map_top,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : S.FG
⊢ S.val.range.FG
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I J : Ideal R[X]
a : R
ha : a ∈ I.leadingCoeff
b : R
⊢ b ∈ J.leadingCoeff → a * b ∈ (I * J).leadingCoeff

Tactic:
hb

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I J : Ideal R[X]
a : R
ha : a ∈ I.leadingCoeff
b : R
hb : b ∈ J.leadingCoeff
⊢ a * b ∈ (I * J).leadingCoeff
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mem_or_mem'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
⊢ ∃ n, (f * g).coeff n ∉ P

Tactic:
classical
        let m := Nat.find hf
        let n := Nat.find hg
        refine ⟨m + n, ?_⟩
        rw [coeff_mul, ← Finset.insert_erase ((Finset.mem_antidiagonal (a := (m, n))).mpr rfl),
          Finset.sum_insert (Finset.notMem_erase _ _), (P.add_mem_iff_left _).not]
        · apply mt h.2
          rw [not_or]
          exact ⟨Nat.find_spec hf, Nat.find_spec hg⟩
        apply P.sum_mem
        rintro ⟨i, j⟩ hij
        rw [Finset.mem_erase, Finset.mem_antidiagonal] at hij
        simp only [Ne, Prod.mk_inj, not_and_or] at hij
        obtain hi | hj : i < m ∨ j < n := by
          lia
        · rw [mul_comm]
          apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hf hi)
        · apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hg hj)

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

Goal state before:
pp: case h.inr
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
⊢ p ∈ Ideal.span ↑s

Tactic:
have hp0 : p ≠ 0 := by
            rintro rfl
            cases hn
            exact Nat.not_lt_zero _ h

Goal state after:
case h.inr
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
⊢ p ∈ Ideal.span ↑s
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
G : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ FiniteType R R[G] ↔ AddGroup.FG G

Tactic:
simpa [AddGroup.fg_iff_addMonoid_fg] using finiteType_iff_fg

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) x) →
          (∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) y) →
            ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) (x * y)

Tactic:
rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
      exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]⟩

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) x) →
          (∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) y) →
            ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) (x * y)

Tactic:
rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
      exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]⟩

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_2.mem.inl
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)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x✝ x : ↥N
hx : x = n
⊢ 0 ∈ M'

Tactic:
exact zero_mem _

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_3.zero
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)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x✝ : ↥M'
x : M
⊢ 0 ∈ ((↑↥A f).domRestrict N').range

Tactic:
exact zero_mem _

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

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
c : Subalgebra R C
⊢ (lift f).range ≤ c ↔ Algebra.adjoin R ↑(NonUnitalAlgHom.range f) ≤ c

Tactic:
rw [lift_range_le, Algebra.adjoin_le_iff]

Goal state after:
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
c : Subalgebra R C
⊢ NonUnitalAlgHom.range f ≤ c.toNonUnitalSubalgebra ↔ ↑(NonUnitalAlgHom.range f) ⊆ ↑c
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
ι : Type u_1
I : ι → Ideal R
inst✝ : ∀ (i : ι), (I i).IsTwoSided
⊢ Injective ⇑(quotientInfToPiQuotient I)

Tactic:
rw [quotientInfToPiQuotient, injective_lift_iff, ker_Pi_Quotient_mk]

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

Goal state before:
pp: x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
⊢ p ∣ p ^ 2

Tactic:
simp [sq]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ¬m = n
a : List α
ha : a ~ m.toList
b : List α
⊢ b ~ n.toList → a ≠ b

Tactic:
hb

Goal state after:
case mpr
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ¬m = n
a : List α
ha : a ~ m.toList
b : List α
hb : b ~ n.toList
⊢ a ≠ b
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: case refine_2.mpr
α : Type u_1
inst✝ : Fintype α
l : List α
⊢ l.Nodup → ∃ a, a.val = ↑l

Tactic:
intro h
      exact CanLift.prf _ h

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 ↦ decide (x = x_1)) l).length + 1
x : α
⊢ count (x :: y :: l) (permutations'Aux x (y :: l)) = (takeWhile (fun x_1 ↦ decide (x = x_1)) (y :: l)).length + 1

Tactic:
permutations'Aux,

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 ↦ decide (x = x_1)) l).length + 1
x : α
⊢ count (x :: y :: l) ((x :: y :: l) :: map (cons y) (permutations'Aux x l)) =
    (takeWhile (fun x_1 ↦ decide (x = x_1)) (y :: l)).length + 1
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
i : ι
h : ¬{n | 0 < n ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}.Nonempty
⊢ minimalPeriod (f i) (x i) ∣ sInf {n | n > 0 ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}

Tactic:
simp [not_nonempty_iff_eq_empty.mp h]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
⊢ [a, l.nextOr a d].length + idxOf a l ≤ l.length

Tactic:
have ⟨_, _⟩ := l.dropLast_prefix

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
w✝ : List α
h✝ : l.dropLast ++ w✝ = l
⊢ [a, l.nextOr a d].length + idxOf a l ≤ l.length
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l ≠ []
hn : l.Nodup
⊢ l.next (l.getLast h) ⋯ = l.head h

Tactic:
have h1 : l.length - 1 + 1 = l.length := by grind [length_pos_iff]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l ≠ []
hn : l.Nodup
h1 : l.length - 1 + 1 = l.length
⊢ l.next (l.getLast h) ⋯ = l.head h
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
l : List α
hl : l.Nodup
⊢ (↑l).Nontrivial ↔ 2 ≤ l.length

Tactic:
Nontrivial

Goal state after:
α : Type u_1
l : List α
hl : l.Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑l ∧ y ∈ ↑l) ↔ 2 ≤ l.length
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
⊢ (∀ (x : α), x ∈ (swap a b)⁻¹ • S ↔ x ∈ S) ↔ (a ∈ S ↔ b ∈ S)

Tactic:
Set.mem_inv_smul_set_iff,

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
hs : Chain r ↑(a :: l)
b : α
⊢ b ∈ ↑(a :: l) → ∀ b_1 ∈ ↑(a :: l), r b b_1

Tactic:
hb

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
hs : Chain r ↑(a :: l)
b : α
hb : b ∈ ↑(a :: l)
⊢ ∀ b_1 ∈ ↑(a :: l), r b b_1
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: ⊢ primeFactorsList 2 = [2]

Tactic:
by simp [primeFactorsList]

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
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (x y : G ⧸ H), ∃ g, g • x = y

Tactic:
{ rintro ⟨x⟩ ⟨y⟩
      refine ⟨y * x⁻¹, QuotientGroup.eq.mpr ?_⟩
      simp only [smul_eq_mul, H.one_mem, inv_mul_cancel, inv_mul_cancel_right]}

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

Goal state before:
pp: n k : ℕ
⊢ ∀ {a : ℕ},
    (∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p) → List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: (k + 2).primeFactorsList)

Tactic:
intro a h

Goal state after:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
⊢ List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: (k + 2).primeFactorsList)
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case h
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ b = (a + 1 + 1) * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod

Tactic:
nth_rw 1 [← Nat.prod_primeFactorsList ha]

Goal state after:
case h
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ b = (a + 1 + 1).primeFactorsList.prod * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a : ZMod (n✝ + 1)
⊢ ↑a.val = a

Tactic:
apply Fin.cast_val_eq_self

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ ↑(-1) = n✝ + 1

Tactic:
· dsimp [ZMod, ZMod.cast]
    rw [Fin.coe_neg_one]

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

Goal state before:
pp: case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ 1 ≤ ↑k

Tactic:
rwa [Fin.ext_iff, Fin.val_zero, ← Ne, ← Nat.one_le_iff_ne_zero] at hk

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ cons n n.properDivisors ⋯ = n.divisors

Tactic:
cons_eq_insert,

Goal state after:
n : ℕ
h : n ≠ 0
⊢ insert n n.properDivisors = n.divisors
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
u : (ZMod 0)ˣ
⊢ (↑u).val.Coprime 0

pp: case succ
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ (↑u).val.Coprime (n + 1)

Tactic:
· rcases Int.units_eq_one_or u with (rfl | rfl) <;> simp

Goal state after:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ (↑u).val.Coprime (n + 1)
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ Set.InjOn (HDiv.hDiv n) ↑n.divisors

Tactic:
intro x hx y hy h
    rw [mem_coe, mem_divisors] at hx hy
    exact (div_eq_iff_eq_of_dvd_dvd hn hx.1 hy.1).mp h

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: q : ℕ
hq : 1 < q
k : ℕ
⊢ map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ }) (antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal

Tactic:
by
  intro k hk
  obtain ⟨i, hi, rfl⟩ := Finset.mem_map.mp hk
  simp [Nat.mem_divisorsAntidiagonal, ← Finset.mem_antidiagonal.mp hi, pow_add, ne_zero_of_lt hq]

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

Goal state before:
pp: n k : ℕ
⊢ (n + 1).ascFactorial k / k ! ≤ (n + 1) ^ k

Tactic:
exact Nat.div_le_of_le_mul (ascFactorial_le_factorial_mul_pow _ _)

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

Goal state before:
pp: n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * 4 ^ n < 4 * (n * n.centralBinom)

Tactic:
by gcongr; exact IH n n.lt_succ_self (Nat.le_of_lt_succ hn)

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

Goal state before:
pp: b k : ℕ
l : List ℕ
⊢ ofDigits b (l ++ List.replicate k 0) = ofDigits b l

Tactic:
rw [ofDigits_append]
  simp

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

Goal state before:
pp: case succ.succ.ind.zero
b : ℕ
h : ∀ m < 0, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits 0) = 0

Tactic:
digits_zero

Goal state after:
case succ.succ.ind.zero
b : ℕ
h : ∀ m < 0, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) [] = 0
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p : ℕ
hp : 1 < p
k : ℕ
⊢ p.maxPowDvdDiv (p ^ k) = (k, 1)

Tactic:
by
  simpa using maxPowDvdDiv_base_pow_mul hp Nat.one_ne_zero k

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

Goal state before:
pp: case h
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
⊢ (n % b :: b.digits (n / b)).length = log b n + 1

Tactic:
List.length

Goal state after:
case h
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
⊢ (b.digits (n / b)).length + 1 = log b n + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case ind.zero
b d : ℕ
IH : ∀ m < 0, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ (b + 2).digits 0
⊢ d < b + 2

Tactic:
digits_zero

Goal state after:
case ind.zero
b d : ℕ
IH : ∀ m < 0, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ []
⊢ d < b + 2
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
p : ℕ
hpos : 0 < p
hd : ℕ
tl : List ℕ
tail_ih✝ : (∀ l ∈ tl, l < p) → ofDigits p tl / p = ofDigits p tl.tail
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ ofDigits p (hd :: tl) / p = ofDigits p (hd :: tl).tail

Tactic:
refine Eq.trans (add_mul_div_left hd _ hpos) ?_
    rw [Nat.div_eq_of_lt <| w₁ _ List.mem_cons_self, zero_add, List.tail_cons]

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

Goal state before:
pp: case e'_2.h
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ (log p n).succ = (p.digits n).length

Tactic:
refine (length_digits p n h hn).symm

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : FiniteMultiplicity a b
⊢ emultiplicity a b = ↑(multiplicity a b)

Tactic:
by
  cases hm : emultiplicity a b
  · simp [h] at hm
  rw [multiplicity_eq_of_emultiplicity_eq_some hm]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hk : ↑k ≤ emultiplicity a b
⊢ a ^ k ∣ b

Tactic:
cases k
  · simp
  unfold emultiplicity at hk
  split at hk
  · norm_cast at hk
    simpa using (Nat.find_min _ (lt_of_succ_le hk))
  · apply FiniteMultiplicity.not_iff_forall.mp ‹_›

Goal state after: