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

Goal state before:
pp: case inr.mpr.refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
c₁ c₂ : R
hmul : p.coeff 0 = c₁ * c₂
hadd : p.coeff 1 = c₁ + c₂
⊢ (X + C c₁) * (X + C c₂) = C (c₁ * c₂) * X ^ 0 + C (c₁ + c₂) * X ^ 1 + C 1 * X ^ 2

Tactic:
C_mul,

Goal state after:
case inr.mpr.refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
c₁ c₂ : R
hmul : p.coeff 0 = c₁ * c₂
hadd : p.coeff 1 = c₁ + c₂
⊢ (X + C c₁) * (X + C c₂) = C c₁ * C c₂ * X ^ 0 + C (c₁ + c₂) * X ^ 1 + C 1 * X ^ 2
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case inr.mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ (∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂) →
    ∃ f g, f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)

Tactic:
· rintro ⟨c₁, c₂, hmul, hadd⟩
      refine
        ⟨X + C c₁, X + C c₂, monic_X_add_C _, monic_X_add_C _, ?_, ?_⟩
      · rw [p.as_sum_range_C_mul_X_pow, hnd, Finset.sum_range_succ, Finset.sum_range_succ,
          Finset.sum_range_one, ← hnd, hm.coeff_natDegree, hnd, hmul, hadd, C_mul, C_add, C_1]
        ring
      · simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
⊢ False

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Goal state after:
case inl
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : IsUnit (X ^ 0 - 1)
⊢ False

case inr
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
hn : n ≠ 0
⊢ False
Module: Mathlib.Algebra.Ring.GeomSum

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

Tactic:
one_pow,

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

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ ↑n
⊢ ∑ n ∈ p.support, (monomial n) (p.coeff n) ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))

Tactic:
refine Submodule.sum_mem _ fun k hk => ?_

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ ↑n
k : ℕ
hk : k ∈ p.support
⊢ (monomial k) (p.coeff k) ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
⊢ ∑ n ∈ p.support, (monomial n) (p.coeff n) ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))

Tactic:
refine Submodule.sum_mem _ fun k hk => ?_

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
k : ℕ
hk : k ∈ p.support
⊢ (monomial k) (p.coeff k) ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ (∃ i, ∃ p ∈ I, p.degree ≤ ↑i ∧ p.leadingCoeff = x) → ∃ p ∈ I, p.leadingCoeff = x

Tactic:
rintro ⟨i, p, hpI, _, rfl⟩

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
i : ℕ
p : R[X]
hpI : p ∈ I
left✝ : p.degree ≤ ↑i
⊢ ∃ p_1 ∈ I, p_1.leadingCoeff = p.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]
⊢ f * g ∈ map C P → f ∈ map C P ∨ g ∈ map C P

Tactic:
simp only [mem_map_C_iff]

Goal state after:
case mem_or_mem'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
⊢ (∀ (n : ℕ), (f * g).coeff n ∈ P) → (∀ (n : ℕ), f.coeff n ∈ P) ∨ ∀ (n : ℕ), g.coeff n ∈ P
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case intro
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
val✝ : Fintype ι
⊢ adjoin S (MvPolynomial.X '' ↑Finset.univ) = ⊤

Tactic:
Finset.coe_univ,

Goal state after:
case intro
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
val✝ : Fintype ι
⊢ adjoin S (MvPolynomial.X '' Set.univ) = ⊤
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case intro
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
val✝ : Fintype ι
⊢ adjoin S (FreeAlgebra.ι S '' ↑Finset.univ) = ⊤

Tactic:
Finset.coe_univ,

Goal state after:
case intro
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
val✝ : Fintype ι
⊢ adjoin S (FreeAlgebra.ι S '' Set.univ) = ⊤
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mpr
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (∃ s f, Surjective ⇑f) → FiniteType R A

Tactic:
· rintro ⟨s, f, hsur⟩
    exact .of_surjective f hsur

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mpr
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ s f, Surjective ⇑f) → FiniteType R S

Tactic:
· rintro ⟨s, f, hsur⟩
    exact .of_surjective f hsur

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 * 1 = coeff 0 i

Tactic:
← h,

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 : ℕ
⊢ p.coeff i * 0 = coeff 0 i
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_1.mem
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} ∪ Set.range nj
⊢ i x ∈ M'

Tactic:
simp only [Set.singleton_union, Set.mem_insert_iff, Set.mem_range] at hx

Goal state after:
case refine_1.mem
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 ∨ ∃ y, nj y = x
⊢ i x ∈ M'
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_2.mem
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} ∪ Set.range nj
⊢ f x ∈ M'

Tactic:
simp only [Set.singleton_union, Set.mem_insert_iff, Set.mem_range] at hx

Goal state after:
case refine_2.mem
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 ∨ ∃ y, nj y = x
⊢ f x ∈ M'
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: a b z : ℤ
⊢ b ≡ a [PMOD z] ↔ a ≡ b [ZMOD z]

Tactic:
simp [modEq_iff_zsmul', dvd_iff_exists_eq_mul_left, Int.ModEq,
    Int.emod_eq_emod_iff_emod_sub_eq_zero, ← Int.dvd_iff_emod_eq_zero]

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

Goal state before:
pp: n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ n ∣ b + d - (a + c)

Tactic:
by convert! Int.dvd_add h₁.dvd h₂.dvd using 1; lia

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

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
hgcd : a.gcd b = 1
⊢ ↑a * a.gcdA b + ↑b * a.gcdB b ≡ 1 [ZMOD ↑b]

Tactic:
rw [← Nat.gcd_eq_gcd_ab, hgcd]

Goal state after:
a b : ℕ
hab : a.Coprime b
hgcd : a.gcd b = 1
⊢ ↑1 ≡ 1 [ZMOD ↑b]
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 : ℕ
⊢ OfNat.ofNat a = OfNat.ofNat b ↔ a % n = b % n

Tactic:
rw [Lean.Grind.Semiring.ofNat_eq_natCast, 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.Data.Nat.Prime.Basic

Goal state before:
pp: p a k : ℕ
hp : Prime (a ^ k)
h : a ^ k = p
⊢ a = p ∧ k = 1

Tactic:
← h,

Goal state after:
p a k : ℕ
hp : Prime (a ^ k)
h : a ^ k = p
⊢ a = a ^ k ∧ k = 1
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ A ∙ (mk I) 1 = Submodule.span A (⇑(Submodule.mkQ I) '' {1})

Tactic:
Set.image_singleton,

Goal state after:
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ A ∙ (mk I) 1 = A ∙ (Submodule.mkQ I) 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
x : A
⊢ (Quotient.lift (ker ↑f) (↑g) H) (↑(quotientKerAlgEquivOfSurjective hf).symm (f x)) = g x

Tactic:
erw [AlgEquiv.coe_toAlgHom]

Goal state after:
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
x : A
⊢ (Quotient.lift (ker ↑f) (↑g) H) ((quotientKerAlgEquivOfSurjective hf).symm (f x)) = g x
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Fintype α
⊢ Finset (List α)

pp: case refine_2
α : Type u_1
inst✝ : Fintype α
⊢ ∀ (x : List α), x ∈ ?refine_1 ↔ x.Nodup

Tactic:
· let univSubsets := ((Finset.univ : Finset α).powerset.1 : (Multiset (Finset α)))
    let allPerms := Multiset.bind univSubsets (fun s => (Multiset.lists s.1))
    refine ⟨allPerms, Multiset.nodup_bind.mpr ?_⟩
    simp only [Multiset.lists_nodup_finset, implies_true, true_and]
    unfold Multiset.Pairwise
    use ((Finset.univ : Finset α).powerset.toList : (List (Finset α)))
    constructor
    · simp only [Finset.coe_toList]
      rfl
    · -- Unfold `List.Nodup` in the type of the proof term to make it match with the goal.
      convert dsimp% [List.Nodup] Finset.nodup_toList (Finset.univ.powerset : Finset (Finset α))
        with m n
      simp only [_root_.Disjoint]
      rw [← m.coe_toList, ← n.coe_toList, Multiset.lists_coe, Multiset.lists_coe]
      have := Multiset.coe_disjoint m.toList.permutations n.toList.permutations
      rw [_root_.Disjoint] at this
      rw [this, List.disjoint_iff_ne]
      constructor
      · intro h
        by_contra hc
        rw [hc] at h
        contrapose! h
        use n.toList
        simp
      · intro h
        simp only [mem_permutations]
        intro a ha b hb
        by_contra hab
        absurd h
        rw [hab] at ha
        exact Finset.perm_toList.mp <| Perm.trans ha.symm hb

Goal state after:
case refine_2
α : Type u_1
inst✝ : Fintype α
⊢ ∀ (x : List α),
    (x ∈
        let univSubsets := Finset.univ.powerset.val;
        let allPerms := univSubsets.bind fun s ↦ s.val.lists;
        { val := allPerms, nodup := ⋯ }) ↔
      x.Nodup
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
⊢ IsPeriodicPt f (minimalPeriod f x) x

Tactic:
delta minimalPeriod

Goal state after:
α : Type u_1
f : α → α
x : α
⊢ IsPeriodicPt f (if h : x ∈ periodicPts f then Nat.find h else 0) x
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
this : ∀ (xs' : List α), (∀ x ∈ xs, x ∈ xs') → d ∈ xs' → xs.nextOr x d ∈ xs'
⊢ d ∈ xs → xs.nextOr x d ∈ xs

Tactic:
by
    exact this xs fun _ => id

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 : StarSubalgebra R A
h : ∀ (x : A), x ∈ S
⊢ S = ⊤

Tactic:
ext x; exact ⟨fun _ => mem_top, fun _ => h x⟩

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

Goal state before:
pp: case cons.succ
α : Type u_1
x y : α
s : List α
IH : ∀ (n : ℕ) (hn : n < (permutations'Aux x s).length), (permutations'Aux x s)[n] = s.insertIdx n x
n✝ : ℕ
hn : n✝ + 1 < (permutations'Aux x (y :: s)).length
⊢ (permutations'Aux x (y :: s))[n✝ + 1] = (y :: s).insertIdx (n✝ + 1) x

Tactic:
· simpa [get] using IH _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ minimalPeriod g x.2 ∣ minimalPeriod (Prod.map f g) x

Tactic:
rw [minimalPeriod_prodMap]; exact Nat.dvd_lcm_right _ _

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

Goal state before:
pp: case cons.left
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
⊢ ∀ (x_1 : List α), x_1 ∈ l.permutations' → (permutations'Aux x x_1).Nodup

Tactic:
intro ys

Goal state after:
case cons.left
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
ys : List α
⊢ ys ∈ l.permutations' → (permutations'Aux x ys).Nodup
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
d x y : α
tail : List α
hl : x :: y :: tail ≠ []
h : (x :: y :: tail).getLast hl ∉ (x :: y :: tail).dropLast
⊢ (x :: y :: tail).nextOr ((x :: y :: tail).getLast hl) d = d

Tactic:
unfold nextOr

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
d x y : α
tail : List α
hl : x :: y :: tail ≠ []
h : (x :: y :: tail).getLast hl ∉ (x :: y :: tail).dropLast
⊢ (if (x :: y :: tail).getLast hl = x then y else (y :: tail).nextOr ((x :: y :: tail).getLast hl) d) = d
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case h
G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
a✝ y : α
yh : y ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
z : α
zh : z ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
⊢ ∃ g, g • ⟨y, yh⟩ = ⟨z, zh⟩

Tactic:
orbitRel.Quotient.mem_orbit,

Goal state after:
case h
G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
a✝ y : α
yh✝ : y ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
yh : Quotient.mk'' y = Quotient.mk'' a✝
z : α
zh✝ : z ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
zh : Quotient.mk'' z = Quotient.mk'' a✝
⊢ ∃ g, g • ⟨y, yh✝⟩ = ⟨z, zh✝⟩
Module: Mathlib.Data.Nat.Prime.Pow

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : k ≠ 0
⊢ (p ^ k).minFac = p

Tactic:
rw [Nat.pow_minFac hk, hp.minFac_eq]

Goal state after:
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)
⊢ Chain r ↑(a :: l)

Tactic:
have Hl : ∀ {b} (_hb : b ∈ l), b ∈ (a :: l : Cycle α) := @fun b hb => by simp [hb]

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)
⊢ Chain r ↑(a :: l)
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case inr
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
H : Subgroup G
inst✝ : Finite (G ⧸ H)
b : X
⊢ Finite (orbitRel.Quotient (↥H) X)

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

Goal state after:
Module: Mathlib.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))
x : { x // x ∈ Quotient.mk (orbitRel G X) ⁻¹' {ω} }
hx : ⟦↑x⟧ = ω
⊢ ↑x ∈ orbitRel.Quotient.orbit ω

Tactic:
orbitRel.Quotient.mem_orbit,

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))
x : { x // x ∈ Quotient.mk (orbitRel G X) ⁻¹' {ω} }
hx : ⟦↑x⟧ = ω
⊢ Quotient.mk'' ↑x = ω
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(ConjClasses.mk g).carrier
inst✝ : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Fintype.card ↑(ConjClasses.mk g).carrier = Fintype.card G / Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
classical
  rw [Fintype.card_congr <| ConjAct.toConjAct (G := G) |>.toEquiv]
  rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct G) g, Nat.mul_div_cancel]
  · simp_rw [ConjAct.orbit_eq_carrier_conjClasses]
  · exact Fintype.card_pos_iff.mpr inferInstance

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

Goal state before:
pp: n k : ℕ
⊢ (n ^ (k + 1)).primeFactors = n.primeFactors

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Goal state after:
case inl
k : ℕ
⊢ (0 ^ (k + 1)).primeFactors = primeFactors 0

case inr
n k : ℕ
hn : n ≠ 0
⊢ (n ^ (k + 1)).primeFactors = n.primeFactors
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_2
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
x : G
y : G'
hy : f y = x
⊢ ∃ a, Quotient.map' ⇑f ⋯ a = Quotient.mk'' x

Tactic:
exact ⟨y, (Quotient.map'_mk'' f _ y).trans (congr_arg Quotient.mk'' hy)⟩

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), (f i).index ≠ 0
⊢ (⨅ i, f i).index ≠ 0

Tactic:
simp_rw [← relIndex_top_right] at hf ⊢

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), (f i).relIndex ⊤ ≠ 0
⊢ (⨅ i, f i).relIndex ⊤ ≠ 0
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:
← Nat.one_le_iff_ne_zero

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