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

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
p✝ : R[X]
p : ℕ
n : R
x✝ :
  eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (Polynomial.C n * Polynomial.X ^ p)) =
    Polynomial.C n * Polynomial.X ^ p
⊢ eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (Polynomial.C n * Polynomial.X ^ (p + 1))) =
    Polynomial.C n * Polynomial.X ^ (p + 1)

Tactic:
Polynomial.eval₂_mul,

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
p✝ : R[X]
p : ℕ
n : R
x✝ :
  eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (Polynomial.C n * Polynomial.X ^ p)) =
    Polynomial.C n * Polynomial.X ^ p
⊢ eval₂ Polynomial.C (fun x ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default) (Polynomial.C n) * Polynomial.eval₂ C (X default) (Polynomial.X ^ (p + 1))) =
    Polynomial.C n * Polynomial.X ^ (p + 1)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ↑n < p.degree ↔ n < p.natDegree

Tactic:
by_cases h : p = 0
  · simp [h]
  simp [degree_eq_natDegree h, Nat.cast_lt]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
⊢ map f p ≠ 0

Tactic:
ne_eq,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
⊢ ¬map f p = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
h4 : map f p ≠ 0
⊢ (map f p).leadingCoeff ≠ 0

Tactic:
ne_eq,

Goal state after:
case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
h4 : map f p ≠ 0
⊢ ¬(map f p).leadingCoeff = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree = 0
⊢ (map f p).natDegree = 0 ↔ f p.leadingCoeff ≠ 0 ∨ True

Tactic:
ne_eq,

Goal state after:
case inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree = 0
⊢ (map f p).natDegree = 0 ↔ ¬f p.leadingCoeff = 0 ∨ True
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
p : R[X]
a : R
inst✝ : NoZeroDivisors R
h₀ : a = 0
⊢ (p * C a).nextCoeff = p.nextCoeff * a

Tactic:
simp [h₀, nextCoeff, natDegree_mul_C]

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
p : R[X]
a : R
inst✝ : NoZeroDivisors R
h₀ : ¬a = 0
⊢ (p * C a).nextCoeff = p.nextCoeff * a

Tactic:
simp [h₀, nextCoeff, natDegree_mul_C]

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

Goal state before:
pp: case h_add
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
o✝ : Option S₁
m₁✝ m₂✝ : ℕ
⊢ (o✝.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ (m₁✝ + m₂✝) =
    (o✝.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₁✝ * (o✝.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₂✝

Tactic:
pow_add

Goal state after:
case h_add
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
o✝ : Option S₁
m₁✝ m₂✝ : ℕ
⊢ (o✝.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₁✝ * (o✝.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₂✝ =
    (o✝.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₁✝ * (o✝.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₂✝
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case monomial
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
j : Option S₁ →₀ ℕ
r : R
n : Option S₁ →₀ ℕ
⊢ coeff n.some (((optionEquivLeft R S₁) ((monomial j) r)).coeff (n none)) = coeff n ((monomial j) r)

Tactic:
| monomial j r =>

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
⊢ ∀ b ∈ (((optionEquivLeft R S₁) p).coeff i).support, (i + b.sum fun x e ↦ e) ≤ p.totalDegree

Tactic:
intro σ

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
σ : S₁ →₀ ℕ
⊢ σ ∈ (((optionEquivLeft R S₁) p).coeff i).support → (i + σ.sum fun x e ↦ e) ≤ p.totalDegree
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 : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
⊢ ∀ b ∈ (((optionEquivLeft R S₁) p).coeff i).support, (b.sum fun x e ↦ e) ≤ p.totalDegree

Tactic:
intro σ

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

Goal state before:
pp: case monomial
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (((finSuccEquiv R n) ((monomial j) r)).coeff i) = coeff (cons i m) ((monomial j) r)

Tactic:
| monomial j r =>

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
h : cons i m ∈ f.support
⊢ m ∈ (((finSuccEquiv R n) f).coeff i).support

Tactic:
simpa [mem_support_iff, ← finSuccEquiv_coeff_coeff m f i] using h

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
⊢ (((finSuccEquiv R n) f).coeff i).support ≠ ∅

Tactic:
ne_eq,

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
⊢ ¬(((finSuccEquiv R n) f).coeff i).support = ∅
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty
⊢ (((finSuccEquiv R n) f).coeff i).totalDegree + i ≤ f.totalDegree

Tactic:
have ⟨σ, hσ1, hσ2⟩ := Finset.exists_mem_eq_sup (support _) hf'_sup
                          (fun s => Finsupp.sum s fun _ e => e)

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty
σ : Fin n →₀ ℕ
hσ1 : σ ∈ (((finSuccEquiv R n) f).coeff i).support
hσ2 : ((((finSuccEquiv R n) f).coeff i).support.sup fun s ↦ s.sum fun x e ↦ e) = σ.sum fun x e ↦ e
⊢ (((finSuccEquiv R n) f).coeff i).totalDegree + i ≤ f.totalDegree
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this✝ : Commute y ((x + y) ^ i)
this : n - (i + 1) + (i + 1) = n
⊢ (x + y) ^ i * y ^ (n - (i + 1) + (i + 1) - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)

Tactic:
add_comm i 1,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this✝ : Commute y ((x + y) ^ i)
this : n - (i + 1) + (i + 1) = n
⊢ (x + y) ^ i * y ^ (n - (1 + i) + (1 + i) - i) = (x + y) ^ i * y ^ (n - (1 + i) + 1)
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₂) = ∑ i ∈ range (p.natDegree + 1), C (p.coeff i) * X ^ i

Tactic:
hnd,

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₂) = ∑ i ∈ range (2 + 1), C (p.coeff i) * X ^ i
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 (p.coeff 0) * X ^ 0 + C (p.coeff 1) * X ^ 1 + C 1 * X ^ p.natDegree

Tactic:
hnd,

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 (p.coeff 0) * X ^ 0 + C (p.coeff 1) * X ^ 1 + C 1 * X ^ 2
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: x y n : ℕ
⊢ x - y ∣ x ^ n - y ^ n

Tactic:
by
  rcases le_or_gt y x with h | h
  · have : y ^ n ≤ x ^ n := Nat.pow_le_pow_left h _
    exact mod_cast sub_dvd_pow_sub_pow (x : ℤ) (↑y) n
  · have : x ^ n ≤ y ^ n := Nat.pow_le_pow_left h.le _
    exact (Nat.sub_eq_zero_of_le this).symm ▸ dvd_zero (x - y)

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
⊢ ↑(p.restriction.coeff n) = p.coeff n

Tactic:
simp only [restriction, coeff_monomial, finsetSum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, ite_not]

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
⊢ ↑(if p.coeff n = 0 then 0 else ⟨p.coeff n, ⋯⟩) = p.coeff n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case insert
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ antidiagonal (i + j)
⊢ (f a).coeff (i, j).1 * (∏ x ∈ s, f x).coeff (i, j).2 ∈ I ^ (n a - i + (∑ x ∈ s, n x - j))

Tactic:
pow_add

Goal state after:
case insert
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ antidiagonal (i + j)
⊢ (f a).coeff (i, j).1 * (∏ x ∈ s, f x).coeff (i, j).2 ∈ I ^ (n a - i) * I ^ (∑ x ∈ s, n x - j)
Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise

Goal state before:
pp: case refine_2
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x : A
hx : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
r : R
⊢ (algebraMap R A) r ∈ toSubmodule S * toSubmodule T

Tactic:
rw [← one_mul (algebraMap _ _ _)]
    exact Submodule.mul_mem_mul (show (1 : A) ∈ S from one_mem S) (algebraMap_mem T _)

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

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
⊢ p ∈ I

Tactic:
rw [as_sum p]

Goal state after:
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
⊢ ∑ v ∈ p.support, (monomial v) (coeff v p) ∈ I
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
x : ι → R
⊢ ∃ r, ∀ (i : ι), r - x i ∈ I i

Tactic:
obtain ⟨y, hy⟩ := Ideal.pi_quotient_surjective hI (fun i ↦ x i)
  exact ⟨y, fun i ↦ (Submodule.Quotient.eq (I i)).mp <| hy i⟩

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
ι✝ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
i j : Fin 2
h : i ≠ j
⊢ (IsCoprime on f) i j

Tactic:
fin_cases i <;> fin_cases j

Goal state after:
case «0».«0»
R✝ : Type u
S : Type v
F : Type w
inst✝³ : Ring R✝
inst✝² : Semiring S
ι✝ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (IsCoprime on f) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
R✝ : Type u
S : Type v
F : Type w
inst✝³ : Ring R✝
inst✝² : Semiring S
ι✝ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (IsCoprime on f) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«0»
R✝ : Type u
S : Type v
F : Type w
inst✝³ : Ring R✝
inst✝² : Semiring S
ι✝ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (IsCoprime on f) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
R✝ : Type u
S : Type v
F : Type w
inst✝³ : Ring R✝
inst✝² : Semiring S
ι✝ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (IsCoprime on f) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: α : 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 α
⊢ (∀ ⦃x : Multiset (List α)⦄, x ≤ m.val.lists → x ≤ n.val.lists → x ≤ ⊥) ↔ ¬m = n

Tactic:
rw [← m.coe_toList, ← n.coe_toList, Multiset.lists_coe, Multiset.lists_coe]

Goal state after:
α : 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 α
⊢ (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔ ¬m = n
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: 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 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

Tactic:
subst e

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

Goal state before:
pp: R : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : StarRing R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : StarRing A
inst✝⁵ : StarModule R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : StarModule R B
ι : Sort u_5
inst✝ : Nonempty ι
f : A →⋆ₐ[R] B
hf : Function.Injective ⇑f
s : ι → StarSubalgebra R A
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
by
  apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hx : x = y
⊢ (y :: z :: l).prev x h = (z :: l).getLast ⋯

Tactic:
by rw [prev, dif_pos hx]

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

Goal state before:
pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
⊢ (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl

Tactic:
by_cases hx : x = hd
    · simp only [hx, prev_cons_cons_eq]
      exact mem_cons_of_mem _ (getLast_mem _)
    · rw [prev, dif_neg hx]
      split_ifs with hm
      · exact mem_cons_self
      · exact mem_cons_of_mem _ (hl _ _)

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

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

Tactic:
rw [Nontrivial]
  rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
  · simp
  · simp
  · simp only [mem_cons, mem_coe_iff, List.length, Ne, Nat.succ_le_succ_iff,
      Nat.zero_le, iff_true]
    refine ⟨hd, hd', ?_, by simp⟩
    simp only [not_or, mem_cons, nodup_cons] at hl
    exact hl.left.left

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

Goal state before:
pp: case h.cons.cons
α : Type u_1
x y : α
hxy : x ≠ y
hd hd' : α
tl : List α
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
hy : y ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl))

Tactic:
simp [Nat.succ_le_succ_iff]

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : R
hn✝ : IsPrimePow n
k : ℕ
hk : k ≠ 0
p : R
k' : ℕ
hp : Prime p
hk' : 0 < k'
hn : p ^ k' = n
⊢ p ^ (k * k') = n ^ k

Tactic:
pow_mul',

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : R
hn✝ : IsPrimePow n
k : ℕ
hk : k ≠ 0
p : R
k' : ℕ
hp : Prime p
hk' : 0 < k'
hn : p ^ k' = n
⊢ (p ^ k') ^ k = n ^ k
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
⊢ Chain r s → ∀ a ∈ s, ∀ b ∈ s, r a b

Tactic:
induction s with
    | nil => exact fun _ b hb ↦ (notMem_nil _ hb).elim
    | cons a l => ?_
    intro hs b hb c hc
    rw [Cycle.chain_coe_cons, List.isChain_iff_pairwise] at hs
    simp only [pairwise_append, pairwise_cons, mem_append, mem_singleton, List.not_mem_nil,
      IsEmpty.forall_iff, imp_true_iff, Pairwise.nil, forall_eq, true_and] at hs
    simp only [mem_coe_iff, mem_cons] at hb hc
    rcases hb with (rfl | hb) <;> rcases hc with (rfl | hc)
    · exact hs.1 c (Or.inr rfl)
    · exact hs.1 c (Or.inl hc)
    · exact hs.2.2 b hb
    · exact _root_.trans (hs.2.2 b hb) (hs.1 c (Or.inl hc))

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

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

Tactic:
rcases b.eq_zero_or_pos with (rfl | hb)

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

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: a b : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ b.primeFactorsList
⊢ a ∣ b

Tactic:
rcases b.eq_zero_or_pos with (rfl | hb)

Goal state after:
case inl
a : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ primeFactorsList 0
⊢ a ∣ 0

case inr
a b : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ b.primeFactorsList
hb : b > 0
⊢ a ∣ b
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
⊢ a ^ (n + 1) ∣ b → replicate (n + 1) a <+~ b.primeFactorsList

Tactic:
rintro ⟨c, rfl⟩

Goal state after:
case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : a ^ (n + 1) * c ≠ 0
⊢ replicate (n + 1) a <+~ (a ^ (n + 1) * c).primeFactorsList
Module: Mathlib.Data.Nat.Factors

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

Tactic:
rcases b.eq_zero_or_pos with (rfl | hb)

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

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.Algebra.Algebra.ZMod

Goal state before:
pp: case zero
R✝ : Type u_1
inst✝² : Ring R✝
R : Type u_2
inst✝¹ : Ring R
x : R
inst✝ : Module (ZMod 0) R
r : ZMod 0
⊢ r • 1 * x = r • x ∧ x * r • 1 = r • x

Tactic:
obtain rfl : ((inferInstance : Module ℤ R)) = ‹_› := Subsingleton.elim _ _

Goal state after:
case zero
R✝ : Type u_1
inst✝¹ : Ring R✝
R : Type u_2
inst✝ : Ring R
x : R
r : ZMod 0
⊢ r • 1 * x = r • x ∧ x * r • 1 = r • x
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ #n.divisors ≤ #(Ico 1 (n + 1))

Tactic:
apply card_le_card

Goal state after:
n : ℕ
⊢ n.divisors ⊆ Ico 1 (n + 1)
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n

Tactic:
rcases Decidable.eq_or_ne n 0 with (rfl | hn)
  · simp
  · rw [← cons_self_properDivisors hn, Finset.sum_cons, add_comm]

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

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (a * 1 + a * (b - 1)) / (b - 1) = a + a / (b - 1)

Tactic:
rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: xy : ℤ × ℤ
z : ℤ
⊢ xy ∈ z.divisorsAntidiag ↔ xy.1 * xy.2 = z ∧ z ≠ 0

Tactic:
rcases z, xy with ⟨_ | _, ⟨_ | _, _ | _⟩⟩
  -- splitting this case saves about 1770 heartbeats i.e. 12.5% faster
  case ofNat.negSucc.negSucc =>
    simp [divisorsAntidiag]
    grind [Nat.cast_inj]
  all_goals
    simp [divisorsAntidiag]
    grind

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

Goal state before:
pp: case inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ (↑n * m + x - x).natAbs

Tactic:
add_sub_cancel_right,

Goal state after:
case inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ (↑n * m).natAbs
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
simp [emultiplicity_eq_zero]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
⊢ (∀ (n : ℕ), a ^ n ∣ b) ↔ a = 1 ∨ b ≤ 0

Tactic:
Nat.le_zero

Goal state after:
a b : ℕ
⊢ (∀ (n : ℕ), a ^ n ∣ b) ↔ a = 1 ∨ b = 0
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: p r i : ℕ
hr : ¬p ∣ r
⊢ (p * i + r).factorization p = 0

Tactic:
by
  apply factorization_eq_zero_of_not_dvd
  rwa [← Nat.dvd_add_iff_right (Dvd.intro i rfl)]

Goal state after: