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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
t : Multiset R[X]
inst✝ : Nontrivial R
h : ∀ f ∈ t, f.Monic
this : t.prod ≠ 0
⊢ t.prod.degree = (Multiset.map degree t).sum

Tactic:
degree_eq_natDegree this,

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
t : Multiset R[X]
inst✝ : Nontrivial R
h : ∀ f ∈ t, f.Monic
this : t.prod ≠ 0
⊢ ↑t.prod.natDegree = (Multiset.map degree t).sum
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
n✝ : ℕ
⊢ ∑ i ∈ range (n✝ + 1), x ^ i * y ^ (n✝ + 1 - 1 - i) = ∑ i ∈ range (n✝ + 1), y ^ i * x ^ (n✝ + 1 - 1 - i)

Tactic:
simp only [Nat.add_sub_cancel]

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
⊢ ∑ x_1 ∈ range (n✝ + 1), x ^ x_1 * y ^ (n✝ - x_1) = ∑ x_1 ∈ range (n✝ + 1), y ^ x_1 * x ^ (n✝ - x_1)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg.h₀
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j✝ : Fin (n + 1)
i : Fin n
hij : i.castSucc < j✝
hj : ¬∃ j₀, j₀.castSucc = j✝
j : Fin n
a✝ : j ∈ univ
hji : j ≠ i
⊢ x j * 0 = 0

Tactic:
mul_zero

Goal state after:
case neg.h₀
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j✝ : Fin (n + 1)
i : Fin n
hij : i.castSucc < j✝
hj : ¬∃ j₀, j₀.castSucc = j✝
j : Fin n
a✝ : j ∈ univ
hji : j ≠ i
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ.refine_3
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
⊢ f =
    ∑ i,
      C (Function.extend Fin.castSucc x (fun x ↦ f.leadingCoeff) i) *
        X ^ Function.extend Fin.castSucc k (fun x ↦ f.natDegree) i

Tactic:
Fin.sum_univ_castSucc

Goal state after:
case succ.refine_3
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
⊢ f =
    ∑ i,
        C (Function.extend Fin.castSucc x (fun x ↦ f.leadingCoeff) i.castSucc) *
          X ^ Function.extend Fin.castSucc k (fun x ↦ f.natDegree) i.castSucc +
      C (Function.extend Fin.castSucc x (fun x ↦ f.leadingCoeff) (Fin.last n)) *
        X ^ Function.extend Fin.castSucc k (fun x ↦ f.natDegree) (Fin.last n)
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).leadingCoeff = k • p.leadingCoeff

Tactic:
Polynomial.leadingCoeff,

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).coeff (k • p).natDegree = k • p.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).coeff (k • p).natDegree = k • p.leadingCoeff

Tactic:
Polynomial.leadingCoeff,

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).coeff (k • p).natDegree = k • p.coeff p.natDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).leadingCoeff = k • p.leadingCoeff

Tactic:
by
  rw [Polynomial.leadingCoeff, Polynomial.leadingCoeff, coeff_smul,
    natDegree_smul_of_smul_regular p h]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
n✝ : ℕ
⊢ (h.unit⁻¹ • (p * q)).coeff n✝ = (h.unit⁻¹ • p * q).coeff n✝

Tactic:
simp only [Units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
n✝ : ℕ
⊢ ∑ i ∈ antidiagonal n✝, ↑h.unit⁻¹ * (p.coeff i.1 * q.coeff i.2) =
    ∑ x ∈ antidiagonal n✝, ↑h.unit⁻¹ * p.coeff x.1 * q.coeff x.2
Module: Mathlib.RingTheory.Polynomial.Basic

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

Tactic:
by
  apply le_antisymm
  · intro p hp
    replace hp := mem_degreeLE.1 hp
    rw [← Polynomial.sum_monomial_eq p, Polynomial.sum]
    refine Submodule.sum_mem _ fun k hk => ?_
    have := WithBot.coe_le_coe.1 (Finset.sup_le_iff.1 hp k hk)
    rw [← C_mul_X_pow_eq_monomial, C_mul']
    refine
      Submodule.smul_mem _ _
        (Submodule.subset_span <|
          Finset.mem_coe.2 <|
            Finset.mem_image.2 ⟨_, Finset.mem_range.2 (Nat.lt_succ_of_le this), rfl⟩)
  rw [Submodule.span_le, Finset.coe_image, Set.image_subset_iff]
  intro k hk
  apply mem_degreeLE.2
  exact
    (degree_X_pow_le _).trans (WithBot.coe_le_coe.2 <| Nat.le_of_lt_succ <| Finset.mem_range.1 hk)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
x : R
⊢ ∀ (i : ℕ), 0 * x ^ i = 0

Tactic:
by simp_rw [zero_mul, forall_const]

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

Goal state before:
pp: A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
h✝ : ∀ (x : C), Function.support (f x) ⊆ ↑y
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
hyy :
  span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) * span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) ≤
    span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
⊢ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) = ⊤

Tactic:
convert! restrictScalars_injective A (Algebra.adjoin A (s : Set B)) C _

Goal state after:
case convert_3
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
h✝ : ∀ (x : C), Function.support (f x) ⊆ ↑y
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
hyy :
  span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) * span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) ≤
    span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
⊢ restrictScalars A (span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)) = restrictScalars A ⊤
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.inr
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree = ↑n
⊢ p.leadingCoeff = p.coeff n

Tactic:
Polynomial.leadingCoeff,

Goal state after:
case mp.inr
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree = ↑n
⊢ p.coeff p.natDegree = p.coeff n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mpr.refine_2
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑n
this : p.natDegree + (n - p.natDegree) = n
⊢ (p * X ^ (n - p.natDegree)).coeff n = p.leadingCoeff

Tactic:
Polynomial.leadingCoeff,

Goal state after:
case mpr.refine_2
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑n
this : p.natDegree + (n - p.natDegree) = n
⊢ (p * X ^ (n - p.natDegree)).coeff n = p.coeff p.natDegree
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
x✝ : ∃ p ∈ I, p.degree ≤ ↑0 ∧ p.leadingCoeff = x
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑0
hpx : p.leadingCoeff = x
⊢ C p.leadingCoeff ∈ I

Tactic:
Polynomial.leadingCoeff,

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
x✝ : ∃ p ∈ I, p.degree ≤ ↑0 ∧ p.leadingCoeff = x
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑0
hpx : p.leadingCoeff = x
⊢ C (p.coeff p.natDegree) ∈ I
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ (s.prod f).coeff k ∈ I ^ (s.sum n - k)

Tactic:
induction s using Finset.induction generalizing k with

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

Goal state before:
pp: case refl
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
hp : 0 ∈ I
ih : ∀ m < natDegree 0, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
h : N < natDegree 0
⊢ False

Tactic:
exact Nat.not_lt_zero _ h

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

Goal state before:
pp: 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
h : 0 = 1
i : ℕ
⊢ p.coeff i * 0 = coeff 0 i

Tactic:
mul_zero

Goal state after:
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
h : 0 = 1
i : ℕ
⊢ 0 = coeff 0 i
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommRing R
h : AddMonoid.FG M
⊢ FiniteType R R[M]

Tactic:
obtain ⟨S, hS⟩ := h.fg_top

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommRing R
h : AddMonoid.FG M
S : Finset M
hS : closure ↑S = ⊤
⊢ FiniteType R R[M]
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
a✝ : v ∈ ⊤
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ∃ y ∈ ((aeval f) p).range, ∃ z ∈ ((aeval f) q).range, y + z = v

Tactic:
use aeval f (p * p') v

Goal state after:
case h
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
a✝ : v ∈ ⊤
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ((aeval f) (p * p')) v ∈ ((aeval f) p).range ∧ ∃ z ∈ ((aeval f) q).range, ((aeval f) (p * p')) v + z = v
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ a + -a ≡ b + -b [ZMOD n]

Tactic:
by simp_rw [← sub_eq_add_neg, sub_self]; rfl

Goal state after:
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : AddMonoidWithOne R
S : Type u_2
inst✝² : Semiring S
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : ExpChar S p
⊢ ExpChar (R × S) p

Tactic:
obtain hp | ⟨hp⟩ := ‹ExpChar R p›

Goal state after:
case zero
R : Type u_1
inst✝⁴ : AddMonoidWithOne R
S : Type u_2
inst✝³ : Semiring S
inst✝² : CharZero R
inst✝¹ : ExpChar R 1
inst✝ : ExpChar S 1
⊢ ExpChar (R × S) 1

case 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
⊢ ExpChar (R × S) p
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
a b c : R
⊢ a + b = c ↔ a = c + b

Tactic:
rw [← sub_eq_iff_eq_add, sub_eq_add]

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

Goal state before:
pp: n m : ℕ
h₀ : m ≠ 0
h : m < n.minFac
⊢ n.Coprime m

Tactic:
rw [← not_not (a := n.Coprime m), Prime.not_coprime_iff_dvd]

Goal state after:
n m : ℕ
h₀ : m ≠ 0
h : m < n.minFac
⊢ ¬∃ p, Prime p ∧ p ∣ n ∧ p ∣ m
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
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
⊢ x = p ∧ y = p

Tactic:
obtain hx | hy := hp.dvd_mul.1 pdvdxy <;>
      [skip; rw [And.comm]] <;>
      [skip; rw [mul_comm] at h pdvdxy]

Goal state after:
case inl
x y p : ℕ
hp : Prime p
hx✝ : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ x = p ∧ y = p

case inr
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : y * x = p ^ 2
pdvdxy : p ∣ y * x
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ y = p ∧ x = p
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hfg : IsPeriodicPt (f ∘ g) n x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt f n x

Tactic:
by
  rw [IsPeriodicPt, hco.comp_iterate] at hfg
  exact hfg.left_of_comp hg

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

Goal state before:
pp: case cons
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun x ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' : List α
⊢ (t :: is ++ ts).permutationsAux is' =
    map (fun x ↦ x ++ ts) ((t :: is).permutationsAux is') ++ ts.permutationsAux ((t :: is).reverse ++ is')

Tactic:
simp only [foldr_permutationsAux2, ih, map_flatMap, cons_append, permutationsAux_cons, map_append,
    reverse_cons, append_assoc]
  congr 2
  funext _
  rw [map_permutationsAux2]
  simp +singlePass only [← permutationsAux2_comp_append]
  simp only [id, append_assoc]

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

Goal state before:
pp: case inl.cons
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
a : α
l₂' : List α
p' : l₁ ++ t :: a :: l₂' ~ t :: is
p : l₁ ++ a :: l₂' ~ is
⊢ (∃ is' x, l₁ ++ t :: a :: l₂' ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: a :: l₂' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁_1 l₂, l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ t :: a :: l₂' ++ ts = l₁_1 ++ t :: l₂ ++ ts

Tactic:
· exact Or.inr (Or.inr ⟨l₁, a :: l₂', mem_permutations_of_perm_lemma (IH2 _) p, by simp⟩)

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

Goal state before:
pp: α : Type u_1
s t : List α
p : s ~ t
⊢ s.permutations' ~ t.permutations'

Tactic:
by
  induction p with
  | nil => simp
  | cons _ _ IH => exact IH.flatMap_right _
  | swap =>
    dsimp
    rw [flatMap_assoc, flatMap_assoc]
    apply Perm.flatMap_left
    intro l' _
    apply perm_permutations'Aux_comm
  | trans _ _ IH₁ IH₂ => exact IH₁.trans IH₂

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 β
m : M
inst✝ : DecidableEq β
b : β
⊢ Decidable ((fun b ↦ b ∈ fixedBy β m) b)

Tactic:
by
  simp only [MulAction.mem_fixedBy]
  infer_instance

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 α
inst✝¹ : Finite G
inst✝ : Finite Ω
⊢ Finite α

Tactic:
by
  rw [(selfEquivSigmaOrbits' G _).finite_iff]
  have : ∀ g : Ω, Finite g.orbit := by
    intro g
    induction g using Quotient.inductionOn'
    simpa [Set.finite_coe_iff] using Finite.finite_mulAction_orbit _
  exact Finite.instSigma

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

Goal state before:
pp: G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
H : Subgroup G
ω : Quotient (orbitRel G X)
q : Quotient (Setoid.comap Subtype.val (orbitRel (↥H) X))
a b : { x // x ∈ Quotient.mk (orbitRel G X) ⁻¹' {ω} }
h : (orbitRel (↥H) X) ↑a ↑b
⊢ ⟦⟨↑a, ⋯⟩⟧ = ⟦⟨↑b, ⋯⟩⟧

Tactic:
← Quotient.eq'',

Goal state after:
G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
H : Subgroup G
ω : Quotient (orbitRel G X)
q : Quotient (Setoid.comap Subtype.val (orbitRel (↥H) X))
a b : { x // x ∈ Quotient.mk (orbitRel G X) ⁻¹' {ω} }
h : Quotient.mk'' ↑a = Quotient.mk'' ↑b
⊢ ⟦⟨↑a, ⋯⟩⟧ = ⟦⟨↑b, ⋯⟩⟧
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G
⊢ ⋯.choose⁻¹ * g = 1

Tactic:
inv_mul_eq_one,

Goal state after:
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G
⊢ ⋯.choose = g
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inr.inl
a : ℕ
ha : a > 0
hab : a.Coprime 0
⊢ (a * 0).primeFactorsList ~ a.primeFactorsList ++ primeFactorsList 0

pp: case inr.inr
a b : ℕ
hab : a.Coprime b
ha : a > 0
hb : b > 0
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Tactic:
· simp [(coprime_zero_right _).mp hab]

Goal state after:
case inr.inr
a b : ℕ
hab : a.Coprime b
ha : a > 0
hb : b > 0
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inr.inl
a p : ℕ
ha : a > 0
hab : a.Coprime 0
⊢ p ∈ (a * 0).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ primeFactorsList 0

pp: case inr.inr
a b : ℕ
hab : a.Coprime b
p : ℕ
ha : a > 0
hb : b > 0
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList

Tactic:
· simp [(coprime_zero_right _).mp hab]

Goal state after:
case inr.inr
a b : ℕ
hab : a.Coprime b
p : ℕ
ha : a > 0
hb : b > 0
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : H.relIndex ⊤ ≠ 0
hK : K.relIndex ⊤ ≠ 0
⊢ (H ⊓ K).relIndex ⊤ ≠ 0

Tactic:
exact relIndex_inf_ne_zero hH hK

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
⊢ H.index = 1 ∨ H.index = 2

Tactic:
have := Nat.le_succ_iff.mp (Nat.le_of_dvd two_pos hH)

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.index ∣ 2
this : H.index ≤ 1 ∨ H.index = Nat.succ 1
⊢ H.index = 1 ∨ H.index = 2
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
← Nat.cast_sub (Nat.mod_le _ _),

Goal state after:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ ↑(↑a + ↑b - (↑a + ↑b) % (n✝ + 1)) = 0
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
← Nat.cast_sub (Nat.mod_le _ _),

Goal state after:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ ↑(↑a * ↑b - ↑a * ↑b % (n✝ + 1)) = 0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.IsFiniteRelIndex ⊤ ↔ H.FiniteIndex

Tactic:
by
  rw [finiteIndex_iff, isFiniteRelIndex_iff_relIndex_ne_zero, relIndex_top_right]

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 [Nat.cast_sub, Nat.cast_one]
        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 : ℕ
a : ℕ × ℕ
⊢ a.swap ∈ n.divisorsAntidiagonalList ↔ a ∈ n.divisorsAntidiagonalList

Tactic:
by simp [mul_comm]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ {d ∈ Ico 1 1 | d ∣ 1} = ∅

Tactic:
Ico_self,

Goal state after:
⊢ {d ∈ ∅ | d ∣ 1} = ∅
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
⊢ ↑(↑a.val * a.val.gcdA n.succ + ↑n.succ * a.val.gcdB n.succ) = ↑(a.val.gcd n.succ)

Tactic:
rw [← Nat.gcd_eq_gcd_ab a.val n.succ]; rfl

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

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 1
⊢ 1⁻¹ = 1

Tactic:
simpa [ZMod.val_one'' hn] using mul_inv_eq_gcd (1 : ZMod n)

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i ∈ map { toFun := fun d ↦ (d, n / d), inj' := ⋯ } n.divisors, f i.1 i.2 = ∏ i ∈ n.divisors, f i (n / i)

Tactic:
Finset.prod_map

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ x ∈ n.divisors,
      f ({ toFun := fun d ↦ (d, n / d), inj' := ⋯ } x).1 ({ toFun := fun d ↦ (d, n / d), inj' := ⋯ } x).2 =
    ∏ i ∈ n.divisors, f i (n / i)
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
Finset.prod_map

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ x ∈ n.divisorsAntidiagonal, f ((Equiv.prodComm ℕ ℕ).toEmbedding x).1 ((Equiv.prodComm ℕ ℕ).toEmbedding x).2 =
    ∏ i ∈ n.divisors, f (n / i) i
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.mpr.inl
n✝ : ℕ
⊢ n✝ + 1 ∣ 2 * 0

Tactic:
mul_zero

Goal state after:
case succ.mpr.inl
n✝ : ℕ
⊢ n✝ + 1 ∣ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case fst
N : ℕ
inst✝ : NeZero N
p : ZMod N × ℕ
⊢ ((fun n ↦ (↑n, n / N)) ((fun p ↦ p.1.val + N * p.2) p)).1 = p.1

pp: case snd
N : ℕ
inst✝ : NeZero N
p : ZMod N × ℕ
⊢ ((fun n ↦ (↑n, n / N)) ((fun p ↦ p.1.val + N * p.2) p)).2 = p.2

Tactic:
· simp only [add_comm p.1.val, cast_add, cast_mul, natCast_self, zero_mul, natCast_val,
        cast_id', id_eq, zero_add]

Goal state after:
case snd
N : ℕ
inst✝ : NeZero N
p : ZMod N × ℕ
⊢ ((fun n ↦ (↑n, n / N)) ((fun p ↦ p.1.val + N * p.2) p)).2 = p.2