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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ (aeval x) p = ∑ i ∈ range n, p.coeff i • x ^ i

Tactic:
by
  simp_rw [Algebra.smul_def]
  exact eval₂_eq_sum_range' (algebraMap R S) hn x

Goal state after:
Module: Mathlib.Data.DFinsupp.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → Zero (α i)
inst✝² : (i : ι) → Lattice (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ = (↑(f.support ∪ g.support))ᶜ

Tactic:
ext; simp [inf_eq_and_sup_eq_iff]

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

Goal state before:
pp: case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e) →
      ∀ {s : σ →₀ ℕ} {a : R},
        eval₂ f g (p * X n * (monomial s) a) = eval₂ f g (p * X n) * f a * s.prod fun n e ↦ g n ^ e

Tactic:
intro p n ih s a
    exact
      calc (p * X n * monomial s a).eval₂ f g
        _ = (p * monomial (Finsupp.single n 1 + s) a).eval₂ f g := by
          rw [monomial_single_add, pow_one, mul_assoc]
        _ = (p * monomial (Finsupp.single n 1) 1).eval₂ f g * f a * s.prod fun n e => g n ^ e := by
          simp [ih, prod_single_index, prod_add_index, pow_one, pow_add, mul_assoc, mul_left_comm,
            f.map_one]

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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ {p : MvPolynomial σ R}, eval₂ f g (p * q) = eval₂ f g p * eval₂ f g q

Tactic:
apply MvPolynomial.induction_on q
  · simp [eval₂_C, eval₂_mul_C]
  · simp +contextual [mul_add, eval₂_add]
  · simp +contextual [X, eval₂_mul_monomial, ← mul_assoc]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
hs : ↑s.support ⊆ range f
⊢ (killCompl hf) ((monomial s) c) = (monomial (Finsupp.comapDomain f s ⋯)) c

Tactic:
← s.mapDomain_comapDomain f hf hs,

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
hs : ↑s.support ⊆ range f
⊢ (killCompl hf) ((monomial (Finsupp.mapDomain f (Finsupp.comapDomain f s ⋯))) c) =
    (monomial (Finsupp.comapDomain f s ⋯)) c
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case add.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial (↥s) R
t : Finset σ
q : MvPolynomial (↥t) R
⊢ (rename Subtype.val) p + (rename Subtype.val) q =
    (rename Subtype.val) ((rename (Subtype.map id ⋯)) p + (rename (Subtype.map id ⋯)) q)

Tactic:
simp only [rename_rename, map_add]

Goal state after:
case add.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial (↥s) R
t : Finset σ
q : MvPolynomial (↥t) R
⊢ (rename Subtype.val) p + (rename Subtype.val) q =
    (rename (Subtype.val ∘ Subtype.map id ⋯)) p + (rename (Subtype.val ∘ Subtype.map id ⋯)) q
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
⊢ coeffsIn σ M = Submodule.span R {x | ∃ m ∈ M, ∃ i, (monomial i) m = x}

Tactic:
by
  classical
  refine le_antisymm ?_ <| Submodule.span_le.2 ?_
  · rintro p hp
    rw [p.as_sum]
    exact sum_mem fun i hi ↦ Submodule.subset_span ⟨_, hp i, _, rfl⟩
  · rintro _ ⟨m, hm, s, n, rfl⟩ i
    simp
    split <;> simp [hm]

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

Goal state before:
pp: case refine_1.mem_mul_mem
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
r : S
s : σ →₀ ℕ
m : S
hm : m ∈ M
n : S
hn : n ∈ N
⊢ (monomial s) (m * n) ∈ coeffsIn σ M * coeffsIn σ N

Tactic:
rw [← add_zero s, ← monomial_mul]
      apply Submodule.mul_mem_mul <;> simpa

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a b : MvPolynomial σ R
x✝¹ x✝ : σ →₀ ℕ
⊢ ((x✝¹ + x✝).sum fun x e ↦ e) ≤ (x✝¹.sum fun x e ↦ e) + x✝.sum fun x e ↦ e

Tactic:
by simp [Finsupp.sum_add_index']

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

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Multiset σ
c : R
x : MvPolynomial σ R
hx : x ∈ {p | p.degrees ≤ s}
⊢ c • x ∈ {p | p.degrees ≤ s}

Tactic:
dsimp
    rw [Algebra.smul_def]
    refine degrees_mul_le.trans ?_
    simpa [degrees_C] using hx

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

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
⊢ ((rename f) φ).vars ⊆ Finset.image f φ.vars

Tactic:
by
  classical
  intro i hi
  simp only [vars_def, Multiset.mem_toFinset, Finset.mem_image] at hi ⊢
  simpa only [Multiset.mem_map] using degrees_rename _ _ hi

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : ¬q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
apply natDegree_eq_of_le_of_coeff_ne_zero natDegree_comp_le

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : ¬q.natDegree = 0
⊢ (p.comp q).coeff (p.natDegree * q.natDegree) ≠ 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
⊢ ((X - C x) * P).eraseLead.eraseLead = (X - C x) * P.eraseLead

Tactic:
obtain ⟨dP, hdP⟩ := Nat.exists_eq_add_of_le' (two_le_natDegree_of_nextCoeff_eraseLead he h)

Goal state after:
case neg
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
⊢ ((X - C x) * P).eraseLead.eraseLead = (X - C x) * P.eraseLead
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
f : MvPolynomial σ R
φ : R →+* S
a : S
⊢ Polynomial.eval₂ φ a ((uniqueAlgEquiv R σ) f) = eval₂ φ (fun x ↦ a) f

Tactic:
rw [← eval₂_uniqueAlgEquiv]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
by_cases q0 : q.natDegree = 0

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

case neg
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : ¬q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree
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:
intros; rw [pow_add]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
⊢ ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ p.natDegree → (φ (C r * X ^ n)).natDegree = fu (C r * X ^ n).natDegree

pp: case refine_2
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
⊢ ∀ (f g : R[X]),
    f.natDegree < g.natDegree →
      g.natDegree ≤ p.natDegree →
        (φ f).natDegree = fu f.natDegree →
          (φ g).natDegree = fu g.natDegree → (φ (f + g)).natDegree = fu (f + g).natDegree

Tactic:
· intro n r r0 _
    rw [natDegree_C_mul_X_pow _ _ r0, C_mul_X_pow_eq_monomial, φ_mon_nat _ _ r0]

Goal state after:
case refine_2
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
⊢ ∀ (f g : R[X]),
    f.natDegree < g.natDegree →
      g.natDegree ≤ p.natDegree →
        (φ f).natDegree = fu f.natDegree →
          (φ g).natDegree = fu g.natDegree → (φ (f + g)).natDegree = fu (f + g).natDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
h0 : q ≠ 0
hl : q.natDegree < p.natDegree
⊢ ¬p ∣ q

Tactic:
by
  rintro ⟨r, rfl⟩
  rw [hp.natDegree_mul' <| right_ne_zero_of_mul h0] at hl
  exact hl.not_ge (Nat.le_add_right _ _)

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ nextCoeff 1 = 0

Tactic:
← map_one (f := C),

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ (C 1).nextCoeff = 0
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).totalDegree + i ≤ f.totalDegree

Tactic:
have hf'_sup : ((finSuccEquiv R n f).coeff i).support.Nonempty := by
    rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty]
    exact hi
  -- Let σ be a monomial index of ((finSuccEquiv R n p).coeff i) of maximal total degree
  have ⟨σ, hσ1, hσ2⟩ := Finset.exists_mem_eq_sup (support _) hf'_sup
                          (fun s => Finsupp.sum s fun _ e => e)
  -- Then cons i σ is a monomial index of p with total degree equal to the desired bound
  let σ' : Fin (n + 1) →₀ ℕ := cons i σ
  convert! le_totalDegree (s := σ') _
  · rw [totalDegree, hσ2, sum_cons, add_comm]
  · rw [← mem_support_coeff_finSuccEquiv]
    exact hσ1

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

Goal state before:
pp: case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
f g : R[X]
hf : f.Monic
hg : g.Monic
⊢ f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)

Tactic:
he

Goal state after:
case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
f g : R[X]
hf : f.Monic
hg : g.Monic
he : f * g = p
⊢ ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
f g : R[X]
hf : f.Monic
hg : g.Monic
⊢ f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
he

Goal state after:
case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
f g : R[X]
hf : f.Monic
hg : g.Monic
he : f * g = p
⊢ f.natDegree = 0 ∨ g.natDegree = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
⊢ ¬Irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

Tactic:
cases subsingleton_or_nontrivial R

Goal state after:
case inl
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Subsingleton R
⊢ ¬Irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ ¬Irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Ring R
k : ℕ
hk : ∑ i ∈ range k, (-1) ^ i = if Even k then 0 else 1
⊢ ∑ i ∈ range (k + 1), (-1) ^ i = if Even (k + 1) then 0 else 1

Tactic:
simp only [geom_sum_succ', Nat.even_add_one, hk]

Goal state after:
case succ
R : Type u_1
inst✝ : Ring R
k : ℕ
hk : ∑ i ∈ range k, (-1) ^ i = if Even k then 0 else 1
⊢ ((-1) ^ k + if Even k then 0 else 1) = if ¬Even k then 0 else 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Ring R
a : R
n : ℕ
h : n ≠ 0
⊢ (X ^ n - C a).Monic

Tactic:
simpa only [map_neg, ← sub_eq_add_neg] using monic_X_pow_add_C (-a) h

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:
by
  rw [as_sum p]
  suffices ∀ m ∈ p.support, monomial m (MvPolynomial.coeff m p) ∈ I by
    exact Submodule.sum_mem I this
  intro m _
  rw [← mul_one (coeff m p), ← C_mul_monomial]
  suffices C (coeff m p) ∈ I by exact I.mul_mem_right (monomial m 1) this
  simpa [Ideal.mem_comap] using hcoe m

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

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p q : ℕ
inst✝ : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h : ↑q = 0
⊢ False

Tactic:
rw [cast_eq_zero_iff R p q] at h

Goal state after:
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p q : ℕ
inst✝ : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h : p ∣ q
⊢ False
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case h
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (Quotient.mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) (e i) = 0
i : ι
⊢ ∀ (x : ι), x ≠ i → (Quotient.mk (I i)) (f x * e x) = 0

Tactic:
intro j hj
    simp [(he j).2 i hj.symm]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ¬m = n
⊢ ∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b

Tactic:
simp only [mem_permutations]

Goal state after:
case mpr
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ¬m = n
⊢ ∀ (a : List α), a ~ m.toList → ∀ (b : List α), b ~ n.toList → a ≠ b
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ f^[n] x ∈ periodicPts f

Tactic:
· rcases hx with ⟨m, hm, hx⟩
    exact ⟨m, hm, hx.apply_iterate n⟩

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

Goal state before:
pp: case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x / (minimalPeriod f x).gcd n * (minimalPeriod f x).gcd n ∣
    minimalPeriod f^[n] x * (n / (minimalPeriod f x).gcd n) * (minimalPeriod f x).gcd n

Tactic:
rw [Nat.div_mul_cancel (gcd_dvd_left _ _), mul_assoc, Nat.div_mul_cancel (gcd_dvd_right _ _),
      mul_comm]

Goal state after:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x ∣ n * minimalPeriod f^[n] x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ ∃ n, f^[n] x = x

Tactic:
by
  simpa only [← mem_periodicOrbit_iff hx] using! iterate_mem_periodicOrbit hx 0

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
i : ι
⊢ minimalPeriod (f i) (x i) ∣ minimalPeriod (Pi.map f) x

Tactic:
by
  simp only [minimalPeriod_piMap]
  by_cases h : {n | 0 < n ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}.Nonempty
  · exact (Nat.sInf_mem h).2 i
  · simp [not_nonempty_iff_eq_empty.mp h]

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

Goal state before:
pp: α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : s.length = t.length
⊢ s.insertIdx s.length x = t.insertIdx s.length x

Tactic:
rw [← get_permutations'Aux s x s.length (by simp),
    ← get_permutations'Aux t x s.length (by simp [hl])]

Goal state after:
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : s.length = t.length
⊢ (permutations'Aux x s).get ⟨s.length, ⋯⟩ = (permutations'Aux x t).get ⟨s.length, ⋯⟩
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn✝ : n < (hd :: tl).length
hn : n < tl.length + 1
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (n + (1 + tl.length)) % (tl.length + 1) = n

Tactic:
add_comm 1,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn✝ : n < (hd :: tl).length
hn : n < tl.length + 1
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (n + (tl.length + 1)) % (tl.length + 1) = n
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:
rw [(selfEquivSigmaOrbits' G _).finite_iff]

Goal state after:
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Finite G
inst✝ : Finite Ω
⊢ Finite ((ω : Ω) × ↑ω.orbit)
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : Fintype G
inst✝¹ : (g : G) → Fintype ↑(fixedBy X g)
inst✝ : Fintype (Quotient (orbitRel G X))
⊢ ∑ g, Fintype.card ↑(fixedBy X g) = Fintype.card (Quotient (orbitRel G X)) * Fintype.card G

Tactic:
rw [← Fintype.card_prod, ← Fintype.card_sigma,
    Fintype.card_congr (sigmaFixedByEquivOrbitsProdGroup G X)]

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

Goal state before:
pp: case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ≤ n

Tactic:
· exact le_of_dvd hn (dvd_of_mem_primeFactorsList h)

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.normalCore = (MulAction.toPermHom G (G ⧸ H)).ker

Tactic:
apply le_antisymm
  · intro g hg
    apply Equiv.Perm.ext
    refine fun q ↦ QuotientGroup.induction_on q ?_
    refine fun g' => (MulAction.Quotient.smul_mk H g g').trans (QuotientGroup.eq.mpr ?_)
    rw [smul_eq_mul, mul_inv_rev, ← inv_inv g', inv_inv]
    exact H.normalCore.inv_mem hg g'⁻¹
  · refine (Subgroup.normal_le_normalCore.mpr fun g hg => ?_)
    rw [← H.inv_mem_iff, ← mul_one g⁻¹, ← QuotientGroup.eq, ← mul_one g]
    exact (MulAction.Quotient.smul_mk H g 1).symm.trans (Equiv.Perm.ext_iff.mp hg (1 : G))

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

Goal state before:
pp: a : ℤ
b : ℕ
⊢ a ≡ 0 [ZMOD ↑b] ↔ ↑b ∣ a

Tactic:
Int.modEq_zero_iff_dvd

Goal state after:
a : ℤ
b : ℕ
⊢ ↑b ∣ a ↔ ↑b ∣ a
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
h : K ≤ L
inst✝ : H.IsFiniteRelIndex L
⊢ H.IsFiniteRelIndex K

Tactic:
rw [isFiniteRelIndex_iff_relIndex_ne_zero]
  exact mt (relIndex_eq_zero_of_le_right h) relIndex_ne_zero

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

Goal state before:
pp: case neg.zero
R : Type u_1
inst✝ : Ring R
k : ZMod 0
hk : ¬k = 0
⊢ (k - 1).cast = k.cast - 1

Tactic:
dsimp [ZMod, ZMod.cast]
      rw [Int.cast_sub, Int.cast_one]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y : G
| #(map (Equiv.toEmbedding (Equiv.mulRight y⁻¹))
      (filter ((fun g ↦ f g = f x) ∘ ⇑(Equiv.toEmbedding (Equiv.mulRight y⁻¹))) univ))

Tactic:
card_map

Goal state after:
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y : G
| #(filter ((fun g ↦ f g = f x) ∘ ⇑(Equiv.toEmbedding (Equiv.mulRight y⁻¹))) univ)
Module: Mathlib.Algebra.Polynomial.Cardinal

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ #R[X] ≤ max #R ℵ₀

Tactic:
cases subsingleton_or_nontrivial R

Goal state after:
case inl
R : Type u
inst✝ : Semiring R
h✝ : Subsingleton R
⊢ #R[X] ≤ max #R ℵ₀

case inr
R : Type u
inst✝ : Semiring R
h✝ : Nontrivial R
⊢ #R[X] ≤ max #R ℵ₀
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.divisorsAntidiagonalList.reverse = List.map Prod.swap n.divisorsAntidiagonalList

Tactic:
by
  have : Std.Asymm (α := ℕ × ℕ) (·.snd < ·.snd) := ⟨fun _ _ ↦ lt_asymm⟩
  refine List.Perm.eq_of_pairwise' pairwise_divisorsAntidiagonalList_snd.reverse
    (pairwise_divisorsAntidiagonalList_fst.map _ fun _ _ ↦ id) ?_
  simp [List.reverse_perm', List.perm_ext_iff_of_nodup nodup_divisorsAntidiagonalList
    (nodup_divisorsAntidiagonalList.map Prod.swap_injective), mul_comm]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n

Tactic:
· rw [← cons_self_properDivisors hn, Finset.sum_cons, add_comm]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x ∈ p.divisors, f x = f p * f 1

Tactic:
by
  rw [← cons_self_properDivisors h.ne_zero, prod_cons, h.prod_properDivisors]

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

Goal state before:
pp: case succ.mp.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 * a.val = 0
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

Tactic:
mul_eq_zero

Goal state after:
case succ.mp.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 = 0 ∨ a.val = 0
⊢ a = 0 ∨ 2 * a.val = n✝ + 1
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p n : ℕ
⊢ p ^ padicValNat p n * n.divMaxPow p = n

Tactic:
by
  rw [Nat.mul_comm, divMaxPow_mul_pow_padicValNat]

Goal state after: