mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
⊢ (φ ^ n).vars ⊆ φ.vars

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ']
    apply Finset.Subset.trans (vars_mul _ _)
    exact Finset.union_subset (Finset.Subset.refl _) ih

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

Goal state before:
pp: case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
⊢ degreeOf i (p + q) ≤ degreeOf i p

Tactic:
← max_eq_left_of_lt h

Goal state after:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
⊢ degreeOf i (p + q) ≤ max (degreeOf i p) (degreeOf i q)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ (p + q).totalDegree ≤ p.totalDegree

Tactic:
← max_eq_left_of_lt h

Goal state after:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ (p + q).totalDegree ≤ max p.totalDegree q.totalDegree
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
c : R
⊢ (C c).nextCoeffUp = 0

Tactic:
nextCoeffUp

Goal state after:
R : Type u
inst✝ : Semiring R
c : R
⊢ (if (C c).natTrailingDegree = 0 then 0 else (C c).coeff ((C c).natTrailingDegree + 1)) = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n✝ : ℕ
h₁ : c = n✝ + 1
⊢ #f.eraseLead.support + 1 = n✝ + 1

Tactic:
rw [eraseLead_support, card_erase_of_mem (natDegree_mem_support_of_nonzero h), ← hc, h₁]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n✝ : ℕ
h₁ : c = n✝ + 1
⊢ n✝ + 1 - 1 + 1 = n✝ + 1
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case insert.inr.inl
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (f x).degree = (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs)
      · simp
      obtain ⟨y, hy, hy'⟩ := Finset.exists_mem_eq_sup s hs fun i => degree (f i)
      rw [IH, hy'] at H
      by_cases hx0 : f x = 0
      · simp [hx0, IH]
      have hy0 : f y ≠ 0 := by
        contrapose! H
        simpa [H, degree_eq_bot] using hx0
      refine absurd H (h ?_ ?_ fun H => hx ?_)
      · simp [hx0]
      · simp [hy, hy0]
      · exact H.symm ▸ hy

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : 1 < #f.support
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0

Tactic:
left

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : 1 < #f.support
⊢ f.eraseLead.natDegree < f.natDegree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
s : S₁
⊢ (sumRingEquiv R S₁ S₂).symm (X s) = X (Sum.inl s)

Tactic:
simp [← sumRingEquiv_X_inl]

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
df : p.natDegree < n
⊢ (p - q).coeff n = -q.coeff n

Tactic:
rwa [sub_eq_add_neg, coeff_add_eq_right_of_lt, coeff_neg]

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ C (p.coeff 1) * X + C (p.coeff 0) = p

Tactic:
ext n
    obtain _ | _ | n := n
    · simp
    · simp
    · simp only [coeff_add, coeff_mul_X, coeff_C_succ, add_zero]
      rw [coeff_eq_zero_of_natDegree_lt]
      simp [hp]

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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = (X - C x) * P.eraseLead

Tactic:
by_cases hp : P = 0
  · simp [hp]
  -- can assume eraseLead P ≠ 0, otherwise it's a monomial and both sides are zero.
  by_cases he : P.eraseLead = 0
  · rw [he, mul_zero]
    by_cases he₂ : ((X - C x) * P).eraseLead = 0
    · simp [he₂]
    suffices #((X - C x) * P).support ≤ 2 by
      rw [← card_support_eq_zero]
      linarith [eraseLead_support_card_lt he₂,
        eraseLead_support_card_lt (mul_ne_zero (X_sub_C_ne_zero x) hp)]
    have h₂ : #(X - C x).support = 2 := by
      simpa [← sub_eq_add_neg] using!
        card_support_binomial one_ne_zero one_ne_zero (neg_ne_zero.mpr hx)
    have hmul := card_support_mul_le (p := X - C x) (q := P)
    rw [h₂] at hmul
    linarith [card_support_le_one_of_eraseLead_eq_zero he]
  have h₁ : ((X - C x) * P).natDegree = P.natDegree + 1 := by
    rw [natDegree_mul (X_sub_C_ne_zero x) hp, natDegree_X_sub_C, add_comm]
  -- 2 ≤ P.natDegree
  obtain ⟨dP, hdP⟩ := Nat.exists_eq_add_of_le' (two_le_natDegree_of_nextCoeff_eraseLead he h)
  -- the subleading term of (X - C η) * P is nonzero
  have h₂ : ((X - C x) * P).nextCoeff ≠ 0 := by
    simp only [nextCoeff, hdP, Nat.succ_ne_zero, ite_false, Nat.add_one_sub_one] at h
    rw [nextCoeff, h₁, add_tsub_cancel_right, hdP, coeff_X_sub_C_mul]
    simp [h, hx, ← hdP, hp]
  -- Prove equality by showing coefficients are equal
  ext n
  rcases n.lt_or_ge P.natDegree with hn | hn
  · --n < P.natDegree
    have hd₁ : n < ((X - C x) * P).eraseLead.natDegree := by
      linarith [natDegree_eraseLead_add_one h₂]
    rw [← self_sub_monomial_natDegree_leadingCoeff, coeff_sub, coeff_monomial, if_neg hd₁.ne']
    rw [← self_sub_monomial_natDegree_leadingCoeff, coeff_sub, coeff_monomial, if_neg (by lia)]
    rw [← self_sub_monomial_natDegree_leadingCoeff, mul_sub, coeff_sub,
      sub_zero, sub_zero, eq_sub_iff_add_eq, add_eq_left]
    rcases hn₂ : n
    · simpa [coeff_monomial, hp] using! fun _ ↦ by lia
    · rw [coeff_X_sub_C_mul, coeff_monomial, coeff_monomial, if_neg (by lia),
        if_neg (by lia), mul_zero, sub_zero]
  · --n ≥ P.natDegree, so all the coefficients are zero.
    trans 0 <;> rw [coeff_eq_zero_of_natDegree_lt]
    · grw [eraseLead_natDegree_le, eraseLead_natDegree_le]
      simpa [h₁, hdP] using! hn
    · grw [natDegree_mul (X_sub_C_ne_zero x) he, natDegree_eraseLead_le_of_nextCoeff_eq_zero h]
      simpa [add_comm, hdP] using! hn

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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
s : S₁ → R
y : R
f : MvPolynomial (Option S₁) R
φ : (MvPolynomial S₁ R)[X] →ₐ[R] R[X] :=
  let __src := Polynomial.mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ (aeval fun x ↦ x.elim y s) (X none) = ((Polynomial.aeval y).comp (φ.comp ↑(optionEquivLeft R S₁))) (X none) ∧
    ∀ (x : S₁),
      (aeval fun x ↦ x.elim y s) (X (Option.some x)) =
        ((Polynomial.aeval y).comp (φ.comp ↑(optionEquivLeft R S₁))) (X (Option.some x))

Tactic:
simp only [aeval_X, Option.elim_none, AlgHom.coe_comp, Polynomial.coe_aeval_eq_eval,
    AlgHom.coe_mk, Polynomial.coe_mapRingHom, AlgEquiv.coe_toAlgHom, comp_apply,
    optionEquivLeft_apply, Polynomial.map_X, Polynomial.eval_X, Option.elim_some,
    Polynomial.map_C, eval_X, Polynomial.eval_C, implies_true, and_self, φ]

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

Goal state before:
pp: case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
⊢ (((optionEquivLeft R S₁) p).coeff i).totalDegree + i ≤ p.totalDegree

Tactic:
rw [totalDegree, add_comm, Finset.add_sup (by simpa only [support_nonempty]), Finset.sup_le_iff]

Goal state after:
case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
⊢ ∀ b ∈ (((optionEquivLeft R S₁) p).coeff i).support, (i + b.sum fun x e ↦ e) ≤ p.totalDegree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case neg.refine_1
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ (i + σ.sum fun x e ↦ e) ≤ (embDomain Embedding.some σ + Finsupp.single none i).sum fun x e ↦ e

Tactic:
simp [Finsupp.sum_add_index, Finsupp.sum_embDomain, add_comm i]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
⊢ (∑ x_1, if k j = k x_1 then x x_1 else 0) ≠ 0

Tactic:
rw [sum_eq_single_of_mem j (mem_univ j), if_pos rfl]

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
⊢ x j ≠ 0

case refine_2
R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
⊢ ∀ b ∈ univ, b ≠ j → (if k j = k b then x b else 0) = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
i : σ
r : R
⊢ (toMvPolynomial i) (C r) = MvPolynomial.C r

Tactic:
simp [toMvPolynomial]

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

Goal state before:
pp: R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ (toMvPolynomial i) X = MvPolynomial.X i

Tactic:
simp [toMvPolynomial]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x y : R
hxy : y ≤ x
n : ℕ
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

Tactic:
apply eq_tsub_of_add_eq
  simpa only [tsub_add_cancel_of_le hxy] using geom_sum₂_mul_add (x - y) y n

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : ¬p = 0
⊢ ↑(k • p).natDegree = p.degree

Tactic:
← degree_eq_natDegree,

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : ¬p = 0
⊢ (k • p).degree = p.degree

case neg
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : ¬p = 0
⊢ k • p ≠ 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
n✝ : ℕ
ih : ∀ m < n✝, ∀ f ∈ I, f.natDegree = m → f ∈ map C (comap C I)
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n✝
h : C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I)
⊢ f ∈ map C (comap C I)

Tactic:
rcases f.eraseLead_natDegree_lt_or_eraseLead_eq_zero with hlt | hzero

Goal state after:
case h.inl
R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
n✝ : ℕ
ih : ∀ m < n✝, ∀ f ∈ I, f.natDegree = m → f ∈ map C (comap C I)
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n✝
h : C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I)
hlt : f.eraseLead.natDegree < f.natDegree
⊢ f ∈ map C (comap C I)

case h.inr
R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
n✝ : ℕ
ih : ∀ m < n✝, ∀ f ∈ I, f.natDegree = m → f ∈ map C (comap C I)
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n✝
h : C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I)
hzero : f.eraseLead = 0
⊢ f ∈ map C (comap C I)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ∃ s f, Surjective ⇑f

Tactic:
use s, MvPolynomial.aeval (↑)

Goal state after:
case h
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ Surjective ⇑(MvPolynomial.aeval Subtype.val)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ MvPolynomial (Fin 0) R ≃+* R

Tactic:
apply MvPolynomial.isEmptyRingEquiv R (Fin 0)

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

Goal state before:
pp: case inl
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ -(c * a) ≡ -(c * b) [ZMOD -(c * n)]

Tactic:
← Int.neg_mul,

Goal state after:
case inl
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ -(c * a) ≡ -(c * b) [ZMOD -c * n]
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: case inl
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ -(c * a) ≡ -(c * b) [ZMOD -c * n]

Tactic:
← Int.neg_mul,

Goal state after:
case inl
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ -c * a ≡ -(c * b) [ZMOD -c * n]
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: case refine_1
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m / ↑d ∣ (b - a) * c / ↑(m.gcd c)

Tactic:
Int.sub_mul

Goal state after:
case refine_1
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m / ↑d ∣ (b * c - a * c) / ↑(m.gcd c)
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: a b : ℕ
⊢ ↑a * a.gcdA b ≡ ↑(a.gcd b) [ZMOD ↑b]

Tactic:
by
  rw [← add_zero ((a : ℤ) * _), Nat.gcd_eq_gcd_ab]
  exact (dvd_mul_right _ _).zero_modEq_int.add_left _

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
g : S → R
hf : Function.RightInverse g ⇑f
⊢ Function.LeftInverse (⇑(Ideal.Quotient.mk (ker f)) ∘ g) ⇑f.kerLift

Tactic:
rintro ⟨x⟩

Goal state after:
case mk
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
g : S → R
hf : Function.RightInverse g ⇑f
x✝ : R ⧸ ker f
x : R
⊢ (⇑(Ideal.Quotient.mk (ker f)) ∘ g) (f.kerLift (Quot.mk (⇑(Submodule.quotientRel (ker f))) x)) =
    Quot.mk (⇑(Submodule.quotientRel (ker f))) x
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: case prime.prime
R : Type u_1
inst✝³ : AddMonoidWithOne R
S : Type u_2
inst✝² : Semiring S
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : ExpChar S p
hp : Nat.Prime p
hchar✝¹ : CharP R p
hprime✝ : Nat.Prime p
hchar✝ : CharP S p
⊢ ExpChar (R × S) p

Tactic:
have := Prod.charP R S p; exact .prime hp

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

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ Odd p ↔ 3 ≤ p

Tactic:
rw [← not_iff_not, not_odd_iff_even, hp.even_iff, not_le]
  grind [hp.two_le]

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

Goal state before:
pp: case mp
α : 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 : ∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b
hc : m = n
⊢ False

Tactic:
rw [hc] at h

Goal state after:
case mp
α : 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 : ∀ a ∈ n.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b
hc : m = n
⊢ False
Module: Mathlib.Data.List.Cycle

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

Tactic:
rcases xs with - | ⟨z, zs⟩
  · rfl
  · exact if_neg h

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

Goal state before:
pp: α : Type u_1
f : α → α
inst✝ : Finite α
h : periodicPts f = univ
⊢ Injective f

Tactic:
Finite.injective_iff_surjective,

Goal state after:
α : Type u_1
f : α → α
inst✝ : Finite α
h : periodicPts f = univ
⊢ Surjective f
Module: Mathlib.Data.List.Permutation

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

Tactic:
induction l generalizing x with
  | nil => simp [takeWhile, count]
  | cons y l IH =>
    rw [permutations'Aux, count_cons_self]
    by_cases hx : x = y
    · subst hx
      simpa [takeWhile, Nat.succ_inj, DecEq_eq] using IH _
    · rw [takeWhile]
      simp only [mem_map, cons.injEq, Ne.symm hx, false_and, and_false, exists_false,
        not_false_iff, count_eq_zero_of_not_mem, Nat.zero_add, hx, decide_false, length_nil]

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:
getElem_pmap,

Goal state after:
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
⊢ l.next l[i✝] ⋯ = (l.rotate 1)[i✝]
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < (pmap l.prev l ⋯).length
hn' : n < (l.rotate (l.length - 1)).length
⊢ (pmap l.prev l ⋯)[n] = l[(n + (l.length - 1)) % l.length]

Tactic:
getElem_pmap,

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < (pmap l.prev l ⋯).length
hn' : n < (l.rotate (l.length - 1)).length
⊢ l.prev l[n] ⋯ = l[(n + (l.length - 1)) % l.length]
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 - ↑1 = 0

Tactic:
← smul_eq_zero_iff_left hx,

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
⊢ (↑g - ↑1) • x = 0
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
x✝³ x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ (x✝³ • x✝²)⁻¹ * x✝³ • x✝¹ ∈ H

Tactic:
by rwa [smul_eq_mul, smul_eq_mul, mul_inv_rev, mul_assoc, inv_mul_cancel_left]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : Std.Antisymm r
hs : ∀ a ∈ s, ∀ b ∈ s, r a b
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b

Tactic:
exact antisymm (hs a ha b hb) (hs b hb a ha)

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

Goal state before:
pp: case inl.zero
n2 : 2 < 2 ^ 0
⊢ 4 ∣ 2 ^ 0 ∨ ∃ p, Prime p ∧ p ∣ 2 ^ 0 ∧ Odd p

pp: case inl.succ.zero
n2 : 2 < 2 ^ (0 + 1)
⊢ 4 ∣ 2 ^ (0 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (0 + 1) ∧ Odd p

pp: case inl.succ.succ
k : ℕ
n2 : 2 < 2 ^ (k + 1 + 1)
⊢ 4 ∣ 2 ^ (k + 1 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (k + 1 + 1) ∧ Odd p

pp: case inr
n : ℕ
n2 : 2 < n
p : ℕ
hp : Prime p
hdvd : p ∣ n
hodd : Odd p
⊢ 4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p

Tactic:
· contradiction

Goal state after:
case inl.succ.zero
n2 : 2 < 2 ^ (0 + 1)
⊢ 4 ∣ 2 ^ (0 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (0 + 1) ∧ Odd p

case inl.succ.succ
k : ℕ
n2 : 2 < 2 ^ (k + 1 + 1)
⊢ 4 ∣ 2 ^ (k + 1 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (k + 1 + 1) ∧ Odd p

case inr
n : ℕ
n2 : 2 < n
p : ℕ
hp : Prime p
hdvd : p ∣ n
hodd : Odd p
⊢ 4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inl.succ.zero
n2 : 2 < 2 ^ (0 + 1)
⊢ 4 ∣ 2 ^ (0 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (0 + 1) ∧ Odd p

pp: case inl.succ.succ
k : ℕ
n2 : 2 < 2 ^ (k + 1 + 1)
⊢ 4 ∣ 2 ^ (k + 1 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (k + 1 + 1) ∧ Odd p

pp: case inr
n : ℕ
n2 : 2 < n
p : ℕ
hp : Prime p
hdvd : p ∣ n
hodd : Odd p
⊢ 4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p

Tactic:
· contradiction

Goal state after:
case inl.succ.succ
k : ℕ
n2 : 2 < 2 ^ (k + 1 + 1)
⊢ 4 ∣ 2 ^ (k + 1 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (k + 1 + 1) ∧ Odd p

case inr
n : ℕ
n2 : 2 < n
p : ℕ
hp : Prime p
hdvd : p ∣ n
hodd : Odd p
⊢ 4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hHK : H ≤ K
hKL : K ≤ L
⊢ H.relIndex K * K.relIndex L = H.relIndex L

Tactic:
rw [← relIndex_subgroupOf hKL]
  exact relIndex_mul_index fun x hx => hHK hx

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

Goal state before:
pp: a n : ℕ
a0 : a ≠ 0
⊢ addOrderOf ↑a = n / n.gcd a

Tactic:
by
  rw [← Nat.smul_one_eq_cast, addOrderOf_nsmul' _ a0, ZMod.addOrderOf_one]

Goal state after:
Module: Mathlib.GroupTheory.Index

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

Tactic:
obtain (hH | hH) : H.index = 1 ∨ H.index = 2 := by
      -- This is just showing that 2 is prime, but we do it "longhand" to avoid making any
      -- dependence on number theory files.
      have := Nat.le_succ_iff.mp (Nat.le_of_dvd two_pos hH)
      rw [Nat.le_one_iff_eq_zero_or_eq_one, or_assoc] at this
      exact this.resolve_left fun h ↦ (two_ne_zero <| Nat.zero_dvd.mp (h ▸ hH)).elim

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH✝ : H.index ∣ 2
hH : H.index = 1
⊢ ∃ a, ∀ (b : G), b * a ∈ H ∨ b ∈ H

case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH✝ : H.index ∣ 2
hH : H.index = 2
⊢ ∃ a, ∀ (b : G), b * a ∈ H ∨ b ∈ H
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
n : ℕ
h : 0 = n + 1
⊢ ZMod 0 ≃+* ZMod (n + 1)

pp: case succ.zero
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
m : ℕ
h : m + 1 = 0
⊢ ZMod (m + 1) ≃+* ZMod 0

pp: case succ.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
⊢ ZMod (m + 1) ≃+* ZMod (n + 1)

Tactic:
· exfalso
    exact n.succ_ne_zero h.symm

Goal state after:
case succ.zero
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
m : ℕ
h : m + 1 = 0
⊢ ZMod (m + 1) ≃+* ZMod 0

case succ.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
⊢ ZMod (m + 1) ≃+* ZMod (n + 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x y : ZMod n
⊢ (x + y).cast = (x.cast + y.cast) % ↑n

Tactic:
by
  rw [← ZMod.coe_intCast, Int.cast_add, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]

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
⊢ ↑↑(k - 1) = ↑↑k - 1

Tactic:
rw [Fin.coe_sub_one, if_neg]

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

case neg.succ.hnc
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ¬k = 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n ∉ n.properDivisors

Tactic:
simp [properDivisors]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inl
n : ℕ
⊢ n ∈ properDivisors 0 ↔ n ∣ 0 ∧ n < 0

Tactic:
simp [properDivisors]

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

Goal state before:
pp: n : ℕ
⊢ (2 * n).choose n ≤ 2 ^ (2 * n)

Tactic:
choose_le_two_pow

Goal state after:
n : ℕ
⊢ 2 ^ (2 * n) ≤ 2 ^ (2 * n)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
hm : NeZero m
h : m ≤ n
a : ZMod m
this : NeZero n
⊢ ↑a.cast.val = a

Tactic:
val_cast_eq_val_of_lt (a.val_lt.trans_le h),

Goal state after:
m n : ℕ
hm : NeZero m
h : m ≤ n
a : ZMod m
this : NeZero n
⊢ ↑a.val = a