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

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
⊢ (↑(sumAlgEquiv R S₁ S₂)).comp (rename Sum.inl) = mapAlgHom (Algebra.ofId R (MvPolynomial S₂ R))

Tactic:
ext; simp

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

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q : R[X]
hq : 0 < q.degree
⊢ degree 0 = degree 0 * q.degree

Tactic:
degree_zero,

Goal state after:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q : R[X]
hq : 0 < q.degree
⊢ ⊥ = ⊥ * q.degree
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: ι : Type w
S : Type u_1
inst✝ : Semiring S
f : ι → S[X]
s : Finset ι
d : WithBot ℕ
hd : ∀ k ∈ s, (f k).degree = d
hf : ∑ k ∈ s, (f k).leadingCoeff ≠ 0
⊢ (∑ k ∈ s, f k).leadingCoeff = ∑ k ∈ s, (f k).leadingCoeff

Tactic:
obtain _ | d := d

Goal state after:
case none
ι : Type w
S : Type u_1
inst✝ : Semiring S
f : ι → S[X]
s : Finset ι
hf : ∑ k ∈ s, (f k).leadingCoeff ≠ 0
hd : ∀ k ∈ s, (f k).degree = none
⊢ (∑ k ∈ s, f k).leadingCoeff = ∑ k ∈ s, (f k).leadingCoeff

case some
ι : Type w
S : Type u_1
inst✝ : Semiring S
f : ι → S[X]
s : Finset ι
hf : ∑ k ∈ s, (f k).leadingCoeff ≠ 0
d : ℕ
hd : ∀ k ∈ s, (f k).degree = some d
⊢ (∑ k ∈ s, f k).leadingCoeff = ∑ k ∈ s, (f k).leadingCoeff
Module: Mathlib.Algebra.Polynomial.Monic

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

Tactic:
exact h f g (hg.of_mul_monic_left hp) hg (mul_comm f g) hdg

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ f 1 ≠ 0

Tactic:
map_one

Goal state after:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ 1 ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case left
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsLeftRegular p

pp: case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsRightRegular p

Tactic:
· intro q r h
    dsimp only at h
    rw [← sub_eq_zero, ← hp.mul_right_eq_zero_iff, mul_sub, h, sub_self]

Goal state after:
case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsRightRegular p
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝ : Semiring R
n : ℕ
p q : ↥(degreeLT R n)
⊢ (fun n_1 ↦ (↑(p + q)).coeff ↑n_1) = (fun n_1 ↦ (↑p).coeff ↑n_1) + fun n_1 ↦ (↑q).coeff ↑n_1

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝ : Semiring R
n : ℕ
x : R
p : ↥(degreeLT R n)
⊢ (fun n_1 ↦ (↑(x • p)).coeff ↑n_1) = (RingHom.id R) x • fun n_1 ↦ (↑p).coeff ↑n_1

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : C x ∈ I
hx0 : ¬x = 0
y : R
hy : x * y = 1
⊢ 1 = C 1

Tactic:
map_one

Goal state after:
R : Type u
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : C x ∈ I
hx0 : ¬x = 0
y : R
hy : x * y = 1
⊢ 1 = 1
Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite

Goal state before:
pp: R : Type u_2
inst✝ : NonAssocSemiring R
s : Set R
⊢ sInf (Subsemiring.unop ⁻¹' {S | s ⊆ ↑S}) = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}

Tactic:
Set.preimage_ofPred_eq,

Goal state after:
R : Type u_2
inst✝ : NonAssocSemiring R
s : Set R
⊢ sInf {a | s ⊆ ↑a.unop} = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}
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
k : ℕ
h : N < k
x✝ : R
hx : x✝ ∈ I.leadingCoeffNth k
hxm : x✝ ∉ M
⊢ ¬M < I.leadingCoeffNth k

Tactic:
by
              refine WellFounded.not_lt_min inst.wf _ ?_; exact ⟨k, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.MulOpposite

Goal state before:
pp: R : Type u_2
inst✝ : NonAssocRing R
s : Set R
⊢ sInf (Subring.unop ⁻¹' {S | s ⊆ ↑S}) = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}

Tactic:
Set.preimage_ofPred_eq,

Goal state after:
R : Type u_2
inst✝ : NonAssocRing R
s : Set R
⊢ sInf {a | s ⊆ ↑a.unop} = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_2
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 : ↥N
hx : x ∈ N'
⊢ (↑↥A f) x ∈ M'

Tactic:
induction hx using span_induction with
    | mem x hx =>
      change f x ∈ M'
      simp only [Set.singleton_union, Set.mem_insert_iff, Set.mem_range] at hx
      rcases hx with hx | ⟨j, rfl⟩
      · rw [hx, hn]; exact zero_mem _
      · exact subset_span (by simp [hnj])
    | zero => simp
    | add x _ y _ hx hy => rw [map_add]; exact add_mem hx hy
    | smul a x _ hx => rw [map_smul]; exact smul_mem _ _ hx

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

Goal state before:
pp: a b : ℕ
⊢ ↑a * a.gcdA b + 0 ≡ ↑a * a.gcdA b + ↑b * a.gcdB b [ZMOD ↑b]

Tactic:
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
hf : Function.Surjective ⇑f
⊢ (quotientKerEquivOfSurjective hf).symm.toRingHom.comp f = Ideal.Quotient.mk (ker f)

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
α : Type u_2
inst✝² : Semiring α
inst✝¹ : IsLeftCancelAdd α
n : ℕ
inst✝ : CharP α n
a b : ℕ
⊢ ↑a = OfNat.ofNat b ↔ a % n = b % n

Tactic:
Lean.Grind.Semiring.ofNat_eq_natCast

Goal state after:
R : Type u_1
α : Type u_2
inst✝² : Semiring α
inst✝¹ : IsLeftCancelAdd α
n : ℕ
inst✝ : CharP α n
a b : ℕ
⊢ ↑a = ↑b ↔ a % n = b % n
Module: Mathlib.Algebra.CharP.Two

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

Tactic:
by
  rw [← CharTwo.sub_eq_add, sub_eq_iff_eq_add, zero_add]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
x y : R
⊢ (x + y) * (x + y) = x * x + y * y

Tactic:
by
  rw [← pow_two, ← pow_two, ← pow_two, add_sq]

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

Goal state before:
pp: R₁ : Type u_1
A : Type u_3
inst✝⁵ : CommSemiring R₁
inst✝⁴ : Ring A
inst✝³ : Algebra R₁ A
I J : Ideal A
inst✝² : I.IsTwoSided
inst✝¹ : J.IsTwoSided
hIJ : I ≤ J
K : Ideal A
inst✝ : K.IsTwoSided
hJK : J ≤ K
⊢ ((factorₐ R₁ hJK).comp (factorₐ R₁ hIJ)).comp (mkₐ R₁ I) = (factorₐ R₁ ⋯).comp (mkₐ R₁ I)

Tactic:
ext; simp

Goal state after:
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)
⊢ r • f 1 = r • 1

Tactic:
map_one

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)
⊢ r • 1 = r • 1
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

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

Tactic:
ext; simp

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

Goal state before:
pp: p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
hpd4 : p ∣ m / p ^ k * (n / p ^ l)
hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l
this : p ^ k * p ∣ m ∨ p ^ l * p ∣ n
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n

Tactic:
_root_.pow_succ,

Goal state after:
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
hpd4 : p ∣ m / p ^ k * (n / p ^ l)
hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l
this : p ^ k * p ∣ m ∨ p ^ l * p ∣ n
⊢ p ^ k * p ∣ m ∨ p ^ (l + 1) ∣ n
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts : List α
r L : List (List α)
l' : List α
this :
  (∃ a, a ∈ L ∧ ∃ l₁ l₂, ¬l₂ = [] ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ l₁ l₂, ¬l₂ = [] ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts)
⊢ l' ∈ foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) r L ↔
    l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts

Tactic:
rw [foldr_permutationsAux2]

Goal state after:
α : Type u_1
t : α
ts : List α
r L : List (List α)
l' : List α
this :
  (∃ a, a ∈ L ∧ ∃ l₁ l₂, ¬l₂ = [] ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ l₁ l₂, ¬l₂ = [] ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts)
⊢ l' ∈ flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) L ++ r ↔
    l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ IsPeriodicPt f m x

Tactic:
suffices n ≤ (n / r + 1) * r by
    unfold IsPeriodicPt IsFixedPt
    convert! (hm.apply_iterate ((n / r + 1) * r - n)).eq <;>
      rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]

Goal state after:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ n ≤ (n / r + 1) * r
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
inst✝ : Subsingleton α
⊢ minimalPeriod f x = 1

Tactic:
simp [nontriviality]

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

Goal state before:
pp: α : 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 α
p : l ~ is ++ t :: ts
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts

Tactic:
rcases IH1 _ (p.trans perm_middle) with (⟨is', p', e⟩ | m)

Goal state after:
case inl
α : 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 α
p : l ~ is ++ t :: ts
is' : List α
p' : is' ~ t :: is
e : l = is' ++ ts
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts

case inr
α : 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 α
p : l ~ is ++ t :: ts
m : l ∈ ts.permutationsAux (t :: is)
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
⊢ ↑(centralizer R s) ∪ star ↑(centralizer R s) = ↑(Subalgebra.centralizer R (s ∪ star s))

Tactic:
StarMemClass.star_coe_eq

Goal state after:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
⊢ ↑(centralizer R s) ∪ ↑(centralizer R s) = ↑(Subalgebra.centralizer R (s ∪ star s))
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
⊢ ⊤.toSubalgebra = ⊤

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S T : StarSubalgebra R A
⊢ (S ⊓ T).toSubalgebra = S.toSubalgebra ⊓ T.toSubalgebra

Tactic:
ext; simp

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

Goal state before:
pp: α : Type u_1
ts : List α
⊢ ts.permutations ~ ts.permutations'

Tactic:
obtain ⟨n, h⟩ : ∃ n, length ts < n := ⟨_, Nat.lt_succ_self _⟩
  induction n generalizing ts with | zero => cases h | succ n IH => ?_
  refine List.reverseRecOn ts (fun _ => ?_) (fun ts t _ h => ?_) h; · simp [permutations]
  rw [← concat_eq_append, length_concat, Nat.succ_lt_succ_iff] at h
  have IH₂ := (IH ts.reverse (by rwa [length_reverse])).trans (reverse_perm _).permutations'
  simp only [permutations_append, foldr_permutationsAux2, permutationsAux_nil,
    permutationsAux_cons, append_nil]
  refine
    (perm_append_comm.trans ((IH₂.flatMap_right _).append ((IH _ h).map _))).trans
      (Perm.trans ?_ perm_append_comm.permutations')
  rw [map_eq_flatMap, singleton_append, permutations']
  refine (flatMap_append_perm _ _ _).trans ?_
  refine Perm.of_eq ?_
  congr
  funext _
  rw [permutations'Aux_eq_permutationsAux2, permutationsAux2_append]

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

Goal state before:
pp: case pos
α : 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 : α
hx : x = y
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    (takeWhile (fun x_1 ↦ decide (x = x_1)) (y :: l)).length + 1

Tactic:
subst hx
      simpa [takeWhile, Nat.succ_inj, DecEq_eq] using IH _

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

Goal state before:
pp: α : Type u_1
⊢ ↑[].cyclicPermutations = {[]}

Tactic:
cyclicPermutations_nil,

Goal state after:
α : Type u_1
⊢ ↑[[]] = {[]}
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ IsChain r (a :: (l ++ [a]))

Tactic:
apply Pairwise.isChain

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ List.Pairwise r (a :: (l ++ [a]))
Module: Mathlib.GroupTheory.Index

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

Tactic:
suffices ∀ b, b ∈ H by simp [(eq_top_iff' _).mpr this]

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ∨ b ∈ H
ha' : a ∈ H
⊢ ∀ (b : G), b ∈ H
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a : ℕ
x : ZMod a
⊢ (ringEquivCongr ⋯) x = x

Tactic:
by
  rw [ringEquivCongr_refl]
  rfl

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.index → m ∣ n
m : ℕ
hlt : 0 < m
hle : m ≤ H.index
he : a ^ m ∈ H
⊢ a ^ n ∈ H

Tactic:
rcases hn m hlt hle with ⟨k, rfl⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
m : ℕ
hlt : 0 < m
hle : m ≤ H.index
he : a ^ m ∈ H
k : ℕ
hn : ∀ (m_1 : ℕ), 0 < m_1 → m_1 ≤ H.index → m_1 ∣ m * k
⊢ a ^ (m * k) ∈ H
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x✝ : ℤ
⊢ (Int.castAddHom (ZMod n)) x✝ = 0 ↔ ↑n ∣ x✝

Tactic:
Int.coe_castAddHom,

Goal state after:
n : ℕ
x✝ : ℤ
⊢ (fun x ↦ ↑x) x✝ = 0 ↔ ↑n ∣ x✝
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ 0 < ∑ i ∈ range 2, x ^ i ∧ ∑ i ∈ range 2, x ^ i < 1

Tactic:
rw [geom_sum_two]
    exact ⟨hx', (add_lt_iff_neg_right _).2 hx⟩

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

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

Tactic:
calc
      a * a⁻¹ = a * a⁻¹ + n.succ * Nat.gcdB (val a) n.succ := by
        rw [natCast_self, zero_mul, add_zero]
      _ = ↑(↑a.val * Nat.gcdA (val a) n.succ + n.succ * Nat.gcdB (val a) n.succ) := by
        push_cast
        rw [natCast_zmod_val]
        rfl
      _ = Nat.gcd a.val n.succ := by rw [← Nat.gcd_eq_gcd_ab a.val n.succ]; rfl

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mp
n d nd : ℕ
⊢ (d ∣ n ∧ n ≠ 0) ∧ n / d = nd → d * nd = n ∧ n ≠ 0

Tactic:
rintro ⟨⟨⟨k, rfl⟩, hn⟩, rfl⟩

Goal state after:
case mp
d k : ℕ
hn : d * k ≠ 0
⊢ d * (d * k / d) = d * k ∧ d * k ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
u : (ZMod n)ˣ
⊢ ↑u * ↑u⁻¹ = 1

Tactic:
u.mul_inv

Goal state after:
n : ℕ
u : (ZMod n)ˣ
⊢ 1 = 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mp
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
⊢ n1 * n2 = n ∧ ¬n = 0 → ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n

Tactic:
intro ⟨rfl, hn2⟩

Goal state after:
case mp
n N n1 n2 : ℕ
hn2 : ¬n1 * n2 = 0
n_ne_zero : n1 * n2 ≠ 0
hn : n1 * n2 ≤ N
⊢ ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n1 * n2
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: case h.inr.inr
n : ℕ
IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n
hn : 4 < n
⊢ 4 ^ n < n * n.centralBinom

Tactic:
obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := Nat.exists_eq_succ_of_ne_zero (Nat.ne_zero_of_lt hn)

Goal state after:
case h.inr.inr
n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 ^ (n + 1) < (n + 1) * (n + 1).centralBinom
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: x✝ : 0 < 1
⊢ 4 ^ 1 ≤ 2 * 1 * centralBinom 1

Tactic:
simp [centralBinom, choose]

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

Goal state before:
pp: x✝ : 0 < 2
⊢ 4 ^ 2 ≤ 2 * 2 * centralBinom 2

Tactic:
simp [centralBinom, choose]

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

Goal state before:
pp: x✝ : 0 < 3
⊢ 4 ^ 3 ≤ 2 * 3 * centralBinom 3

Tactic:
simp [centralBinom, choose]

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

Goal state before:
pp: case neg
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
hm : ¬m = 0
⊢ val 0 ^ m < n

Tactic:
· simp only [val_zero, ne_eq, hm, not_false_eq_true, zero_pow, Nat.zero_lt_of_lt h]

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

Goal state before:
pp: m n : ℕ
a : ZMod n
ilt : Fact (1 < n)
h : a.val ^ m < n
⊢ (a ^ m).val = a.val ^ m

Tactic:
induction m with
  | zero => simp [ZMod.val_one]
  | succ m ih =>
    have : a.val ^ m < n := by
      obtain rfl | ha := eq_or_ne a 0
      · by_cases hm : m = 0
        · cases hm; simp [ilt.out]
        · simp only [val_zero, ne_eq, hm, not_false_eq_true, zero_pow, Nat.zero_lt_of_lt h]
      · exact lt_of_le_of_lt
         (Nat.pow_le_pow_right (by rwa [gt_iff_lt, ZMod.val_pos]) (Nat.le_succ m)) h
    rw [pow_succ, ZMod.val_mul, ih this, ← pow_succ, Nat.mod_eq_of_lt h]

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

Goal state before:
pp: case neg
b k : ℕ
hb : 1 < b
n : ℕ
h : ¬n = 0
⊢ log b n + 1 ≤ k ↔ n < b ^ k

Tactic:
← log_lt_iff_lt_pow hb h

Goal state after:
case neg
b k : ℕ
hb : 1 < b
n : ℕ
h : ¬n = 0
⊢ log b n + 1 ≤ k ↔ log b n < k
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case neg
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
⊢ n / b.succ.succ ≠ 0

Tactic:
rw [← pos_iff_ne_zero]

Goal state after:
case neg
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
⊢ 0 < n / b.succ.succ
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) ^ (l.length - 1) ≤ ofDigits (b + 2) l.dropLast + (b + 2) ^ (l.length - 1) * l.getLast hl

Tactic:
refine le_trans ?_ (Nat.le_add_left _ _)

Goal state after:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) ^ (l.length - 1) ≤ (b + 2) ^ (l.length - 1) * l.getLast hl
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b m : ℕ
hb : 1 < b
hm : 0 < m
⊢ b.digits (b * m) = 0 :: b.digits m

Tactic:
rw [digits_def' hb (by positivity)]
  simp [mul_div_right m (by positivity)]

Goal state after:
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
⊢ hd / p + ofDigits p tl = ofDigits p (hd :: tl).tail

Tactic:
Nat.div_eq_of_lt <| w₁ _ List.mem_cons_self,

Goal state after:
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
⊢ 0 + ofDigits p tl = ofDigits p (hd :: tl).tail
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≠ 1
⊢ multiplicity a b = n → emultiplicity a b = ↑n

Tactic:
· intro h₂
    simpa [multiplicity, WithTop.untopD_eq_iff, h] using! h₂

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
⊢ 0 < emultiplicity a b ↔ 0 < multiplicity a b

Tactic:
by
  simp [pos_iff_ne_zero, pos_iff_ne_zero, emultiplicity_eq_zero_iff_multiplicity_eq_zero]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Semiring α
p a b : α
a✝ : ℕ
hm : min (emultiplicity p a) (emultiplicity p b) = ↑a✝
⊢ ↑a✝ ≤ emultiplicity p (a + b)

Tactic:
apply le_emultiplicity_of_pow_dvd

Goal state after:
case coe
α : Type u_1
inst✝ : Semiring α
p a b : α
a✝ : ℕ
hm : min (emultiplicity p a) (emultiplicity p b) = ↑a✝
⊢ p ^ a✝ ∣ a + b