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

Goal state before:
pp: case refine_2.inr.inr
R : Type u
inst✝ : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
hn : p.natDegree < n
⊢ p.coeff n = if n = p.natDegree then 1 else 0

Tactic:
· rw [if_neg hn.ne', coeff_eq_zero_of_natDegree_lt hn]

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

Goal state before:
pp: case zero.succ
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
by_cases g0 : g = 0
      · rw [g0, reflect_zero, mul_zero, mul_zero, reflect_zero]
      rw [← eraseLead_add_C_mul_X_pow g, mul_add, reflect_add, reflect_add, mul_add, hcg, hcg] <;>
        try assumption
      · exact le_add_left card_support_C_mul_X_pow_le_one
      · exact le_trans (natDegree_C_mul_X_pow_le g.leadingCoeff g.natDegree) Og
      · exact Nat.lt_succ_iff.mp (lt_of_lt_of_le (eraseLead_support_card_lt g0) Cg)
      · exact le_trans eraseLead_natDegree_le_aux Og

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
df : p.natDegree < n
⊢ (-q).coeff n = -q.coeff n

pp: R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
df : p.natDegree < n
⊢ p.natDegree < n

Tactic:
coeff_neg

Goal state after:
R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
df : p.natDegree < n
⊢ -q.coeff n = -q.coeff n

R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
df : p.natDegree < n
⊢ p.natDegree < n
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ (algebraMap R (MvPolynomial S₁ R)[X]) r *
      ((none.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m none *
        m.some.prod fun a k ↦ ((Option.some a).elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ k) =
    (Polynomial.monomial (m none)) (C r * m.some.prod fun n e ↦ X n ^ e)

Tactic:
← Polynomial.C_mul_X_pow_eq_monomial

Goal state after:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ (algebraMap R (MvPolynomial S₁ R)[X]) r *
      ((none.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m none *
        m.some.prod fun a k ↦ ((Option.some a).elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ k) =
    Polynomial.C (C r * m.some.prod fun n e ↦ X n ^ e) * Polynomial.X ^ m none
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)
⊢ p.comp q = 0

Tactic:
rw [h.2, comp_C, h.1, C_0]

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

Goal state before:
pp: case inr
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
hp : p ≠ 0
⊢ ↑(p.comp (-X)).natDegree = ↑p.natDegree

Tactic:
Nat.cast_inj,

Goal state after:
case inr
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
hp : p ≠ 0
⊢ (p.comp (-X)).natDegree = p.natDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.degree + q.degree = (q * p).degree

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
hp.degree_mul

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.degree + q.degree = q.degree + p.degree

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q ≠ 0
⊢ (p * q).natDegree = p.natDegree + q.natDegree

Tactic:
natDegree_mul'

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q ≠ 0
⊢ p.natDegree + q.natDegree = p.natDegree + q.natDegree

R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
m : ℕ
d : σ →₀ ℕ
⊢ coeff d (((optionEquivLeft R σ) p).coeff m) = coeff (optionElim m d) p

Tactic:
← optionEquivLeft_coeff_some_coeff_none

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
m : ℕ
d : σ →₀ ℕ
⊢ coeff d (((optionEquivLeft R σ) p).coeff m) =
    coeff (optionElim m d).some (((optionEquivLeft R σ) p).coeff ((optionElim m d) none))
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
n : ℕ
hl : ∀ p ∈ t, p.natDegree ≤ n
⊢ t.prod.coeff (t.card * n) = (Multiset.map (fun p ↦ p.coeff n) t).prod

Tactic:
by
  induction t using Quotient.inductionOn
  simpa using coeff_list_prod_of_natDegree_le _ _ hl

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : ¬p = 0
hp : ∀ (c : ℕ), 1 ≤ p ^ c
⊢ ↑(p ^ a - 1) ∣ ↑(p ^ b - 1)

Tactic:
push_cast [hp a, hp b]

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : ¬p = 0
hp : ∀ (c : ℕ), 1 ≤ p ^ c
⊢ ↑p ^ a - 1 ∣ ↑p ^ b - 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
⊢ q * p = 0 ↔ q = 0

Tactic:
by
  by_cases hq : q = 0 <;> simp [h.mul_left_ne_zero, hq]

Goal state after:
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
⊢ p ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))

Tactic:
← Polynomial.sum_monomial_eq p,

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ ↑n
⊢ (p.sum fun n a ↦ (monomial n) a) ∈ 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
⊢ p ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))

Tactic:
← Polynomial.sum_monomial_eq p,

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support = 3
⊢ ∃ k m n,
    ∃ (_ : k < m) (_ : m < n),
      ∃ x y z, ∃ (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0), f = C x * X ^ k + C y * X ^ m + C z * X ^ n

Tactic:
obtain ⟨k, x, hk, hx, rfl⟩ := card_support_eq.mp h
    refine
      ⟨k 0, k 1, k 2, hk Nat.zero_lt_one, hk (Nat.lt_succ_self 1), x 0, x 1, x 2, hx 0, hx 1, hx 2,
        ?_⟩
    rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc, Fin.sum_univ_one]
    rfl

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

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

Tactic:
grind [geom_sum_mul]

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

Goal state before:
pp: case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a ↦ a • v i
z : A
hz : z ∈ l.support
⊢ ↑(l z) * _root_.id z ∈ span R (p * q)

Tactic:
have : (l z).1 ∈ Subalgebra.toSubmodule (adjoin R s) := (l z).2

Goal state after:
case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this✝ :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a ↦ a • v i
z : A
hz : z ∈ l.support
this : ↑(l z) ∈ Subalgebra.toSubmodule (adjoin R s)
⊢ ↑(l z) * _root_.id z ∈ span R (p * q)
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy this : span B ↑y = ⊤
⊢ ∃ B₀, B₀.FG ∧ ⊤.FG

Tactic:
eq_top_iff',

Goal state after:
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
this : ∀ (x : C), x ∈ span B ↑y
⊢ ∃ B₀, B₀.FG ∧ ⊤.FG
Module: Mathlib.RingTheory.Polynomial.Basic

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

Tactic:
by
  classical
    induction s using Finset.induction generalizing k with
    | empty =>
      rw [sum_empty, prod_empty, coeff_one, zero_tsub, pow_zero, Ideal.one_eq_top]
      exact Submodule.mem_top
    | insert a s ha hs =>
      rw [sum_insert ha, prod_insert ha, coeff_mul]
      apply sum_mem
      rintro ⟨i, j⟩ e
      obtain rfl : i + j = k := mem_antidiagonal.mp e
      apply Ideal.pow_le_pow_right add_tsub_add_le_tsub_add_tsub
      rw [pow_add]
      exact Ideal.mul_mem_mul (by grind) (by grind)

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

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial (↥s) R
hd : C r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
⊢ C r ∣ (rename Subtype.val) a' ∨ C r ∣ (rename Subtype.val) b'

Tactic:
← algebraMap_eq

Goal state after:
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial (↥s) R
hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
⊢ C r ∣ (rename Subtype.val) a' ∨ C r ∣ (rename Subtype.val) b'
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ Surjective ⇑(MvPolynomial.aeval Subtype.val).toRingHom

Tactic:
rw [← Set.range_eq_univ, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, ← AlgHom.coe_range,
    ← Algebra.adjoin_range_eq_range_aeval, Subtype.range_coe_subtype, Finset.setOfPred_mem, hs]

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ↑⊤ = Set.univ
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommRing R
h : AddMonoid.FG M
S : Finset M
hS : closure ↑S = ⊤
⊢ FiniteType R R[M]

Tactic:
exact .of_surjective
      (FreeAlgebra.lift R fun s : (S : Set M) => of' R M ↑s)
      (freeAlgebra_lift_of_surjective_of_closure hS)

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

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroupWithOne G
inst✝ : CharZero G
a b : ℤ
n : ℕ
⊢ ↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [PMOD ↑n]

Tactic:
simpa using intCast_modEq_intCast (G := G) (z := n)

Goal state after:
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 : ι
⊢ (Quotient.mk (I i)) (∑ i, f i * e i) = g i

Tactic:
map_sum,

Goal state after:
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, (Quotient.mk (I i)) (f x * e x) = g i
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I J : Ideal A
h : I ≤ J
⊢ (↑(quotQuotEquivQuotOfLEₐ R h)).comp (Quotient.mkₐ R (map (Quotient.mkₐ R I) J)) = Quotient.factorₐ R h

Tactic:
ext x
  obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
  rfl

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

Goal state before:
pp: case inr
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
left✝ : l₂ ≠ []
m : l₁ ++ l₂ ∈ is.permutationsAux []
⊢ l₁ ++ l₂ ~ is

Tactic:
exact is.append_nil ▸ IH2 _ m

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : x = y
⊢ z = (y :: z :: zs).nextOr y d'

Tactic:
nextOr_self_cons_cons

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : x = y
⊢ z = z
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:
rw [prev, dif_pos hx]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
⊢ l.next a ha = l[(idxOf a l + 1) % l.length]

Tactic:
have hl := ne_nil_of_mem ha

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
hl : l ≠ []
⊢ l.next a ha = l[(idxOf a l + 1) % l.length]
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n : ℕ
h : l ~r l.rotate n
⊢ l[(k + 1) % l.length] = (l.rotate n).next l[k] ⋯

Tactic:
simp_rw [getElem_eq_getElem_rotate _ n k]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n : ℕ
h : l ~r l.rotate n
⊢ l[(k + 1) % l.length] = (l.rotate n).next (l.rotate n)[(l.length - n % l.length + k) % l.length] ⋯
Module: Mathlib.Data.List.Prime

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ (∃ a, a ∈ L ∧ p ∣ a) → p ∣ L.prod

Tactic:
· exact fun ⟨a, ha1, ha2⟩ => dvd_trans ha2 (dvd_prod ha1)

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)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ Chain r ↑(a :: l)

Tactic:
Cycle.chain_coe_cons

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)
⊢ IsChain r (a :: (l ++ [a]))
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:
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.ZMod.Basic

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

Tactic:
dsimp [ZMod, ZMod.cast, ZMod.val]

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

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

Tactic:
dsimp [ZMod, ZMod.cast, ZMod.val]

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

Goal state before:
pp: n m : ℕ
h : m ∣ n
a : ZMod m
⊢ ∃ a_1, (castHom h (ZMod m)) a_1 = a

Tactic:
by obtain ⟨a, rfl⟩ := intCast_surjective a; exact ⟨a, map_intCast ..⟩

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

Goal state before:
pp: a b c : ℕ
hab : a = b
hbc : b = c
⊢ (ringEquivCongr hab).trans (ringEquivCongr hbc) = ringEquivCongr ⋯

Tactic:
subst hab hbc

Goal state after:
a : ℕ
⊢ (ringEquivCongr ⋯).trans (ringEquivCongr ⋯) = ringEquivCongr ⋯
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
dsimp [ZMod, ZMod.cast, ZMod.val]

Goal state after:
case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ↑↑(k - 1) = ↑↑k - 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.divisorsAntidiagonalList.toFinset = n.divisorsAntidiagonal

Tactic:
by
  rw [divisorsAntidiagonalList, divisorsAntidiagonal, List.toFinset_filterMap
    (f_inj := by simp_all), List.toFinset_range'_1_1]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.properDivisors = {1} ↔ Prime n

Tactic:
by
  refine ⟨fun h ↦ ?_, Prime.properDivisors⟩
  rw [Nat.prime_def_lt]
  refine ⟨Nat.succ_le_iff.mpr <| one_mem_properDivisors_iff_one_lt.mp (by simp [h]), ?_⟩
  intro m hm hdvd
  simpa [h] using mem_properDivisors.mpr ⟨hdvd, hm⟩

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
simp (disch := lia) only [le_mul_iff_one_le_right, le_mul_iff_one_le_left, and_true]

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 ∧ 1 ≤ n2) ∧ 0 < n2 ∧ 1 ≤ n1
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: a b n : ℕ
ha : Nat.Prime a
hb : b ≠ 0
⊢ n ≤ padicValNat a b ↔ ↑n ≤ ↑(multiplicity a b)

Tactic:
← padicValNat_def' ha.ne_one hb,

Goal state after:
a b n : ℕ
ha : Nat.Prime a
hb : b ≠ 0
⊢ n ≤ padicValNat a b ↔ ↑n ≤ ↑(padicValNat a b)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ (fixedLengthDigits hb l).card • ∑ x ∈ Finset.range b, x +
      (Finset.range b).card • ∑ x ∈ fixedLengthDigits hb l, x.sum =
    (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
Finset.sum_range_id,

Goal state after:
case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ (fixedLengthDigits hb l).card • (b * (b - 1) / 2) + (Finset.range b).card • ∑ x ∈ fixedLengthDigits hb l, x.sum =
    (l + 1) * b ^ (l + 1 - 1) * b.choose 2
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
H : Type u_6
inst✝ : Monoid H
f : G →* H
hf : Injective ⇑f
x : G
⊢ ∀ (n : ℕ), f (x ^ n) = f 1 ↔ x ^ n = 1

Tactic:
hf.eq_iff,

Goal state after:
G : Type u_1
inst✝¹ : Monoid G
H : Type u_6
inst✝ : Monoid H
f : G →* H
hf : Injective ⇑f
x : G
⊢ ∀ (n : ℕ), True
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ n.centralBinom.factorization p = 0

Tactic:
refine factorization_choose_of_lt_three_mul ?_ p_le_n (p_le_n.trans ?_) big

Goal state after:
case refine_1
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ p ≠ 2

case refine_2
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ n ≤ 2 * n - n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Tactic:
rw [← factorization_le_iff_dvd ha hb, factorization_ordCompl a p, factorization_ordCompl b p]

Goal state after:
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
⊢ Finsupp.erase p a.factorization ≤ Finsupp.erase p b.factorization
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n ↦ x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : s.Finite
⊢ ¬Injective fun n ↦ x ^ n

Tactic:
have := Set.not_injOn_infinite_finite_image (Set.Ioi_infinite 0) h

Goal state after:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n ↦ x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : s.Finite
this : ¬Set.InjOn (fun n ↦ x ^ n) (Set.Ioi 0)
⊢ ¬Injective fun n ↦ x ^ n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ m + k ≡ m [MOD orderOf x] → x ^ (m + k) = x ^ m

Tactic:
intro h
    have hk : x ^ k = 1 := by
      apply pow_eq_one_iff_modEq.2
      exact Nat.ModEq.add_left_cancel' m (by simpa using h)
    calc
      x ^ (m + k) = x ^ m * x ^ k := by rw [pow_add]
      _ = x ^ m := by simp [hk]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
s : Set G := (fun n ↦ x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : s.Finite
⊢ ¬Injective fun n ↦ x ^ n

Tactic:
have := Set.not_injOn_infinite_finite_image (Set.Ioi_infinite 0) h

Goal state after:
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
s : Set G := (fun n ↦ x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : s.Finite
this : ¬Set.InjOn (fun n ↦ x ^ n) (Set.Ioi 0)
⊢ ¬Injective fun n ↦ x ^ n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a✝ : ℕ
⊢ (a.factorization + b.factorization) a✝ = (a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization) a✝

Tactic:
exact (min_add_max _ _).symm

Goal state after: