mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ↑(n.choose (i + 1)) = (∑ i ∈ range n, ↑(n.choose (i + 1)) * X ^ i).coeff i

pp: R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ((∑ i ∈ range n, X ^ i).comp (X + 1)).coeff i = ↑(n.choose (i + 1))

Tactic:
· simp only [finsetSum_coeff, ← C_eq_natCast, coeff_C_mul_X_pow]
    rw [Finset.sum_eq_single i, if_pos rfl]
    · simp +contextual only [@eq_comm _ i, if_false,
        imp_true_iff]
    · simp +contextual only [Nat.lt_add_one_iff, Nat.choose_eq_zero_of_lt,
        Nat.cast_zero, Finset.mem_range, not_lt, if_true, imp_true_iff]

Goal state after:
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ((∑ i ∈ range n, X ^ i).comp (X + 1)).coeff i = ↑(n.choose (i + 1))
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : ⊤.FG
⊢ (map S.val ⊤).FG

Tactic:
exact FG.map _ h

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

Goal state before:
pp: case mp.refine_4
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf : f✝ ∈ map C I
f g : R[X]
hx✝ : g ∈ Submodule.span R[X] (⇑C '' ↑I)
hg : ∀ (n : ℕ), g.coeff n ∈ I
n : ℕ
⊢ (f • g).coeff n ∈ I

Tactic:
smul_eq_mul,

Goal state after:
case mp.refine_4
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf : f✝ ∈ map C I
f g : R[X]
hx✝ : g ∈ Submodule.span R[X] (⇑C '' ↑I)
hg : ∀ (n : ℕ), g.coeff n ∈ I
n : ℕ
⊢ (f * g).coeff n ∈ I
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:
rw [← algebraMap_eq] at hd

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 uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
hA : FiniteType R A
s : Finset A
hS : adjoin R ↑s = ⊤
b : A
le : adjoin R ↑s ≤ Subalgebra.restrictScalars R (adjoin S ↑s)
⊢ b ∈ adjoin S ↑s

Tactic:
exact le (eq_top_iff.1 hS b)

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: 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
⊢ n = 0

Tactic:
choose nj hnj using fun j ↦ hf (mj j)

Goal state after:
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
⊢ n = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case h.inr.convert_2
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
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * X ^ (k - q.natDegree)).leadingCoeff
this : (p - q * X ^ (k - q.natDegree)).degree < ↑p.natDegree
⊢ p - q * X ^ (k - q.natDegree) ∈ Ideal.span ↑s

pp: case h.inr.convert_5
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
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * X ^ (k - q.natDegree)).leadingCoeff
this : (p - q * X ^ (k - q.natDegree)).degree < ↑p.natDegree
⊢ q ∈ Ideal.span ↑s

Tactic:
· by_cases hpq : p - q * Polynomial.X ^ (k - q.natDegree) = 0
            · rw [hpq]
              exact Ideal.zero_mem _
            refine ih _ ?_ (I.sub_mem hp (I.mul_mem_right _ hq)) rfl
            rwa [Polynomial.degree_eq_natDegree hpq, Nat.cast_lt, hn] at this

Goal state after:
case h.inr.convert_5
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
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * X ^ (k - q.natDegree)).leadingCoeff
this : (p - q * X ^ (k - q.natDegree)).degree < ↑p.natDegree
⊢ q ∈ Ideal.span ↑s
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
⊢ Disjoint ((aeval f) p).ker ((aeval f) q).ker

Tactic:
by
  rw [disjoint_iff_inf_le]
  intro v hv
  rcases hpq with ⟨p', q', hpq'⟩
  simpa [LinearMap.mem_ker.1 (Submodule.mem_inf.1 hv).1,
    LinearMap.mem_ker.1 (Submodule.mem_inf.1 hv).2] using
    congr_arg (fun p : R[X] => aeval f p v) hpq'.symm

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

Goal state before:
pp: case mp.refine_4
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f✝ : MvPolynomial σ R
hf : f✝ ∈ Ideal.map C I
f g : MvPolynomial σ R
hx✝ : g ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I)
hg : ∀ (m : σ →₀ ℕ), coeff m g ∈ I
n : σ →₀ ℕ
⊢ coeff n (f • g) ∈ I

Tactic:
smul_eq_mul,

Goal state after:
case mp.refine_4
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f✝ : MvPolynomial σ R
hf : f✝ ∈ Ideal.map C I
f g : MvPolynomial σ R
hx✝ : g ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I)
hg : ∀ (m : σ →₀ ℕ), coeff m g ∈ I
n : σ →₀ ℕ
⊢ coeff n (f * g) ∈ I
Module: Mathlib.GroupTheory.GroupAction.Ring

Goal state before:
pp: case succ
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : R
n : ℕ
ih : (n • x) • y = n • x • y
⊢ (n • x + x) • y = (n • x) • y + x • y

Tactic:
smul_eq_mul,

Goal state after:
case succ
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : R
n : ℕ
ih : (n • x) • y = n • x • y
⊢ (n • x + x) * y = n • x * y + x * y
Module: Mathlib.GroupTheory.GroupAction.Ring

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
n✝ : ℤ
x y : R
n : ℕ
⊢ -((n + 1) • x) • y = -((n + 1) • x • y)

Tactic:
smul_eq_mul,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
n✝ : ℤ
x y : R
n : ℕ
⊢ -((n + 1) • x) * y = -((n + 1) • (x * y))
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ InjOn Int.cast {0, 1, -1}

Tactic:
rintro _ (rfl | rfl | rfl) _ (rfl | rfl | rfl) h <;>
  simp only
    [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢

Goal state after:
case inr.inl.inr.inr
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : 1 = -1
⊢ 1 = -1

case inr.inr.inr.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : -1 = 1
⊢ -1 = 1
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : SetLike S R
hSR : NonUnitalSubsemiringClass S R
s : S
⊢ (unitization s).range = subalgebraOfSubsemiring (Subsemiring.closure ↑s)

Tactic:
by
  have := AddSubmonoidClass.nsmulMemClass (S := S)
  rw [unitization, NonUnitalSubalgebra.unitization_range (hSRA := this), Algebra.adjoin_nat]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : Semiring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : StarModule R A
inst✝¹ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
⊢ (unitization s).range = StarAlgebra.adjoin R ↑s

Tactic:
rw [unitization, Unitization.starLift_range]
  simp only [NonUnitalStarAlgHom.coe_range, NonUnitalStarSubalgebraClass.coe_subtype,
    Subtype.range_coe_subtype]
  rfl

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
I J : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
⊢ ker (quotientMap (map (Quotient.mk I) J) (Quotient.mk I) ⋯) = map (Quotient.mk J) I

Tactic:
by
  rw [Ideal.quotientMap, Ideal.ker_quotient_lift, ← RingHom.comap_ker, Ideal.mk_ker,
    Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective,
    ← RingHom.ker_eq_comap_bot, Ideal.mk_ker, Ideal.map_sup, Ideal.map_quotient_self, bot_sup_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts r ys f).snd = map (fun x ↦ f (x ++ ts)) (permutationsAux2 t [] [] ys id).snd ++ r

Tactic:
← permutationsAux2_append,

Goal state after:
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts [] ys f).snd ++ r = map (fun x ↦ f (x ++ ts)) (permutationsAux2 t [] [] ys id).snd ++ r
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : Type u_1
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) r L =
    flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) L ++ r
⊢ foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) r (l :: L) =
    flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) (l :: L) ++ r

Tactic:
| cons l L ih =>

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

Goal state before:
pp: case cons
α : Type u_1
t : α
ts : List α
r : List (List α)
n : ℕ
l : List α
L : List (List α)
ih : (∀ (l : List α), l ∈ L → l.length = n) → (map length L).sum = n * L.length
H : ∀ (l_1 : List α), l_1 ∈ l :: L → l_1.length = n
⊢ (map length (l :: L)).sum = n * (l :: L).length

Tactic:
| cons l L ih =>

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

Goal state before:
pp: α : Type u_1
f : α → α
n : ℕ
hn : 0 < n
x : α
hx : x ∈ ptsOfPeriod f n
⊢ f (f^[n.pred] x) = x

Tactic:
by
      rw [← comp_apply (f := f), comp_iterate_pred_of_pos f hn, hx.eq]

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

Tactic:
have p := (perm_middle.symm.trans p').cons_inv

Goal state after:
case inl
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ l₂ : List α
p' : l₁ ++ t :: l₂ ~ t :: is
p : l₁ ++ l₂ ~ is
⊢ (∃ is' x, l₁ ++ t :: l₂ ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: l₂ ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁_1 l₂_1, l₁_1 ++ l₂_1 ∈ is.permutations ∧ l₂_1 ≠ [] ∧ l₁ ++ t :: l₂ ++ ts = l₁_1 ++ t :: l₂_1 ++ ts
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case swap
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ : List α
⊢ flatMap (permutations'Aux y✝) (flatMap (permutations'Aux x✝) l✝.permutations') ~
    flatMap (permutations'Aux x✝) (flatMap (permutations'Aux y✝) l✝.permutations')

Tactic:
flatMap_assoc,

Goal state after:
case swap
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ : List α
⊢ flatMap (fun x ↦ flatMap (permutations'Aux y✝) (permutations'Aux x✝ x)) l✝.permutations' ~
    flatMap (permutations'Aux x✝) (flatMap (permutations'Aux y✝) l✝.permutations')
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : 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
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
⊢ (as.insertIdx n x)[m] = x

Tactic:
simp [hn', ← hm']

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

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

Tactic:
by
  constructor
  · intro h
    induction L with
    | nil =>
      rw [prod_nil] at h
      exact absurd h pp.not_dvd_one
    | cons L_hd L_tl L_ih =>
      rw [prod_cons] at h
      rcases pp.dvd_or_dvd h with hd | hd
      · exact ⟨L_hd, mem_cons_self, hd⟩
      · obtain ⟨x, hx1, hx2⟩ := L_ih hd
        exact ⟨x, mem_cons_of_mem L_hd hx1, hx2⟩
  · exact fun ⟨a, ha1, ha2⟩ => dvd_trans ha2 (dvd_prod ha1)

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

Goal state before:
pp: G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
x✝³ x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ (x✝³ • x✝²)⁻¹ * x✝³ • x✝¹ ∈ H

Tactic:
smul_eq_mul,

Goal state after:
G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
x✝³ x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ (x✝³ * x✝²)⁻¹ * x✝³ • x✝¹ ∈ H
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
x✝³ x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ (x✝³ * x✝²)⁻¹ * x✝³ • x✝¹ ∈ H

Tactic:
smul_eq_mul,

Goal state after:
G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
x✝³ x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ (x✝³ * x✝²)⁻¹ * (x✝³ * x✝¹) ∈ H
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : H.Normal
inst✝² : SMul G X
inst✝¹ : MulAction (G ⧸ H) X
inst✝ : IsScalarTower G (G ⧸ H) X
g : G
x : X
⊢ ↑g • x = ↑(g • 1) • x

Tactic:
smul_eq_mul,

Goal state after:
G : Type u
X : Type v
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : H.Normal
inst✝² : SMul G X
inst✝¹ : MulAction (G ⧸ H) X
inst✝ : IsScalarTower G (G ⧸ H) X
g : G
x : X
⊢ ↑g • x = ↑(g * 1) • x
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: ⊢ primeFactorsList 2 = [2]

Tactic:
simp [primeFactorsList]

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

Goal state before:
pp: m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
⊢ m.primeFactors ⊆ n.primeFactors

Tactic:
simp only [subset_iff, mem_primeFactors, and_imp]
  exact fun p hp hpm _ ↦ ⟨hp, hpm.trans hmn, hn⟩

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

Goal state before:
pp: case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
g' : G
⊢ (g • g')⁻¹ * g' ∈ H

Tactic:
smul_eq_mul,

Goal state after:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
g' : G
⊢ (g * g')⁻¹ * g' ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Tactic:
· simp only [ha, true_iff, mul_mem_cancel_left ha]

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
by_cases! hnb : n < b + 2

Goal state after:
case pos
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : n < b + 2
⊢ ((b + 1 + 1).digits n).getLast ⋯ ≠ 0

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

Goal state before:
pp: b : ℕ
l1 l2 : List ℕ
h : l1.length = l2.length
⊢ ofDigits b l1 + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) l1 l2)

Tactic:
by
  induction l1 generalizing l2 with
  | nil => simp_all [eq_comm, List.length_eq_zero_iff, ofDigits]
  | cons hd₁ tl₁ ih₁ =>
    induction l2 generalizing tl₁ with
    | nil => simp_all
    | cons hd₂ tl₂ ih₂ =>
      simp_all only [List.length_cons, ofDigits_cons, add_left_inj,
        eq_comm, List.zipWith_cons_cons]
      rw [← ih₁ h.symm, mul_add]
      ac_rfl

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

Goal state before:
pp: case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) *
      (∑ k ∈ range 1, ofDigits p (List.drop k tl) + (∑ x ∈ Ico 1 tl.length, ofDigits p (List.drop x tl) + 0) +
        ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
← this,

Goal state after:
case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) *
      (∑ k ∈ range 1, ofDigits p (List.drop k tl) +
          (∑ x ∈ Ico 1 tl.length, ofDigits p (List.drop x tl) +
            ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl)) +
        ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
p q : ℕ
h : p ≤ q
head✝ : ℕ
tail✝ : List ℕ
hi : ofDigits p tail✝ ≤ ofDigits q tail✝
⊢ p * ofDigits p tail✝ ≤ q * ofDigits q tail✝

Tactic:
exact Nat.mul_le_mul h hi

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

Goal state before:
pp: p i n : ℕ
h : 2 ≤ p
⊢ n / p ^ i = ofDigits p (List.drop i (p.digits n))

Tactic:
convert!
    ofDigits_div_pow_eq_ofDigits_drop i (zero_lt_of_lt h) (p.digits n)
      (fun l hl ↦ digits_lt_base h hl)
  exact (ofDigits_digits p n).symm

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

Goal state before:
pp: b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ 1 = b' % b

Tactic:
exact h.symm

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

Goal state before:
pp: n i b : ℕ
h : 2 ≤ b + 2
⊢ ((b + 2).digits n).getD i 0 = n / (b + 2) ^ i % (b + 2)

Tactic:
clear h

Goal state after:
n i b : ℕ
⊢ ((b + 2).digits n).getD i 0 = n / (b + 2) ^ i % (b + 2)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : ¬FiniteMultiplicity a a
⊢ multiplicity a a = 1

Tactic:
simp [ha]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d ∣ n ↔ ∃ f ≤ n.factorization, d = f.prod fun x1 x2 ↦ x1 ^ x2

Tactic:
rw [← factorization_le_iff_dvd hd hn]

Goal state after:
n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d.factorization ≤ n.factorization ↔ ∃ f ≤ n.factorization, d = f.prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b p : ℕ
ha : a = 0
⊢ a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)

Tactic:
simp [ha]

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

Goal state before:
pp: n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
⊢ (p * (n + 1))!.factorization p = (p * n)!.factorization p + (n + 1).factorization p + 1

Tactic:
have h2 : p * n + 1 ≤ p * (n + 1) := by linarith

Goal state after:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
⊢ (p * (n + 1))!.factorization p = (p * n)!.factorization p + (n + 1).factorization p + 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ (∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p) ↔ d ∣ n

Tactic:
rw [← factorization_le_iff_dvd hd hn]

Goal state after:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ (∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p) ↔ d.factorization ≤ n.factorization
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
by_cases ha : IsOfFinOrder a

Goal state after:
case pos
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

case neg
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a