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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h✝ : N < k
hp0 : p ≠ 0
h : 0 = 1
⊢ False

Tactic:
apply hp0

Goal state after:
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h✝ : N < k
hp0 : p ≠ 0
h : 0 = 1
⊢ p = 0
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:
disjoint_iff_inf_le

Goal state after:
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
⊢ ((aeval f) p).ker ⊓ ((aeval f) q).ker ≤ ⊥
Module: Mathlib.Algebra.Algebra.Subalgebra.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
⊢ finrank R ↥(A ⊔ B) = finrank R ↥A * finrank ↥A ↥(Algebra.adjoin ↥A ↑B)

Tactic:
by
  simpa only [map_mul] using! congr(Cardinal.toNat $(rank_sup_eq_rank_left_mul_rank_of_free A B))

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

Goal state before:
pp: case mp.refine_1
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ x ∈ ⇑C '' ↑I, ∀ (m : σ →₀ ℕ), coeff m x ∈ I

Tactic:
intro f hf n

Goal state after:
case mp.refine_1
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f✝ : MvPolynomial σ R
hf✝ : f✝ ∈ Ideal.map C I
f : MvPolynomial σ R
hf : f ∈ ⇑C '' ↑I
n : σ →₀ ℕ
⊢ coeff n f ∈ I
Module: Mathlib.RingTheory.Polynomial.Basic

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

Tactic:
simp [I.add_mem (hf n) (hg n)]

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

Goal state before:
pp: a b m n : ℤ
hmn : m.natAbs.Coprime n.natAbs
⊢ a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD m * n]

Tactic:
convert! ← modEq_and_modEq_iff_modEq_lcm using 1

Goal state after:
case e'_2
a b m n : ℤ
hmn : m.natAbs.Coprime n.natAbs
⊢ a ≡ b [ZMOD ↑(m.lcm n)] ↔ a ≡ b [ZMOD m * n]
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: case e'_2
a b m n : ℤ
hmn : m.natAbs.Coprime n.natAbs
⊢ a ≡ b [ZMOD ↑(m.lcm n)] ↔ a ≡ b [ZMOD m * n]

Tactic:
lcm_eq_mul_iff.mpr (.inr <| .inr hmn),

Goal state after:
case e'_2
a b m n : ℤ
hmn : m.natAbs.Coprime n.natAbs
⊢ a ≡ b [ZMOD ↑(m.natAbs * n.natAbs)] ↔ a ≡ b [ZMOD m * n]
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : AddMonoidWithOne R
S : Type u_2
inst✝² : Semiring S
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : ExpChar S p
⊢ ExpChar (R × S) p

Tactic:
obtain hp | ⟨hp⟩ := ‹ExpChar R p›
  · constructor
  obtain _ | _ := ‹ExpChar S p›
  · exact (Nat.not_prime_one hp).elim
  · have := Prod.charP R S p; exact .prime hp

Goal state after:
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
this : SMulMemClass S ℕ R
⊢ Algebra.adjoin ℕ ↑s = subalgebraOfSubsemiring (Subsemiring.closure ↑s)

Tactic:
Algebra.adjoin_nat

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : SetLike S R
hSR : NonUnitalSubsemiringClass S R
s : S
this : SMulMemClass S ℕ R
⊢ subalgebraOfSubsemiring (Subsemiring.closure ↑s) = subalgebraOfSubsemiring (Subsemiring.closure ↑s)
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
a b c : R
⊢ a = b + c ↔ a + c = b

Tactic:
by
  rw [← eq_sub_iff_add_eq, sub_eq_add]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
l : List R
⊢ l.sum * l.sum = (List.map (fun x ↦ x * x) l).sum

Tactic:
by
  simp_rw [← pow_two, list_sum_sq]

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
pp : Prime p
m i : ℕ
⊢ i ∣ p ^ m ↔ ∃ k, k ≤ m ∧ i = p ^ k

Tactic:
simp_rw [_root_.dvd_prime_pow (prime_iff.mp pp) m, associated_eq_eq]

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

Goal state before:
pp: R₁ : Type u_1
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R₁
inst✝³ : Ring A
inst✝² : Algebra R₁ A
inst✝¹ : Semiring B
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
a : A
⊢ (kerLiftAlg f) ((Quotient.mk (ker f)) a) = f a

Tactic:
by
  rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ (quotQuotEquivComm I J).symm = quotQuotEquivComm J I

Tactic:
by
  rfl

Goal state after:
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
⊢ (quotQuotEquivCommₐ R I J).symm = quotQuotEquivCommₐ R J I

Tactic:
by
  rfl

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : NonUnitalStarSubalgebra R A
⊢ Subalgebra.toSubmodule (adjoin R ↑s).toSubalgebra = R ∙ 1 ⊔ s.toSubmodule

Tactic:
adjoin_eq_span,

Goal state after:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : NonUnitalStarSubalgebra R A
⊢ span R ↑(Submonoid.closure (↑s ∪ star ↑s)) = R ∙ 1 ⊔ s.toSubmodule
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case refine_4
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ Function.Surjective fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩

Tactic:
intro ⟨x, hx⟩

Goal state after:
case refine_4
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
x : R ⧸ I ^ (n + 1)
hx : x ∈ map (Quotient.mk (I ^ (n + 1))) (I ^ n)
⊢ ∃ a, (fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩) a = ⟨x, hx⟩
Module: Mathlib.Data.List.Permutation

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

Tactic:
hy.mem_iff

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

Goal state before:
pp: case pos
α : 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
hx : ¬x = hd
hm : x = hd'
⊢ hd ∈ hd :: hd' :: tl

pp: case neg
α : 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
hx : ¬x = hd
hm : ¬x = hd'
⊢ (hd' :: tl).prev x ⋯ ∈ hd :: hd' :: tl

Tactic:
· exact mem_cons_self

Goal state after:
case neg
α : 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
hx : ¬x = hd
hm : ¬x = hd'
⊢ (hd' :: tl).prev x ⋯ ∈ hd :: hd' :: tl
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case neg.e_i
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ idxOf a (head :: tail) - 1 = (idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length

Tactic:
← Nat.add_sub_assoc,

Goal state after:
case neg.e_i
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ idxOf a (head :: tail) - 1 = (idxOf a (head :: tail) + (head :: tail).length - 1) % (head :: tail).length

case neg.e_i.h
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ 1 ≤ (head :: tail).length
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ l.reverse.prev l[k] ⋯ = l.next l[k] hx

Tactic:
← getElem_pmap l.next (fun _ h => h) (by simpa using hk)

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ l.reverse.prev l[k] ⋯ = (pmap l.next l ⋯)[k]
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ IsCancelSMul G α ↔ ∀ (a : α), stabilizer G a = ⊥

Tactic:
by
  simp [isCancelSMul_iff_eq_one_of_smul_eq, Subgroup.eq_bot_iff_forall, forall_comm (α := G)]

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case mpr
n : ℕ
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) → ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
rintro ⟨k, hk, hk', ⟨p, hp, rfl, hp'⟩⟩
    exact ⟨p, k, hp', hk', rfl⟩

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

Goal state before:
pp: G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ (Quotient.out q)⁻¹ * g ^ minimalPeriod (fun x ↦ g • x) q * Quotient.out q ∈ H

Tactic:
rw [mul_assoc, ← QuotientGroup.eq, QuotientGroup.out_eq', ← smul_eq_mul, Quotient.mk_smul_out,
    eq_comm, pow_smul_eq_iff_minimalPeriod_dvd]

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

Goal state before:
pp: G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
g : G ⧸ stabilizer G x
g1 g2 : G
H : (leftRel (stabilizer G x)) g1 g2
⊢ g1 • (g1⁻¹ * g2) • x = g2 • x

Tactic:
by rw [smul_smul, mul_inv_cancel_left]

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

Goal state before:
pp: case refine_2
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ l → _root_.Prime p

Tactic:
simp_rw [← prime_iff]

Goal state after:
case refine_2
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ l → Prime p
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case refine_3
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ n.primeFactorsList → _root_.Prime p

Tactic:
simp_rw [← prime_iff]

Goal state after:
case refine_3
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ n.primeFactorsList → Prime p
Module: Mathlib.Data.Nat.Factors

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

Tactic:
rw [List.subperm_iff]
      rintro ⟨u, hu1, hu2⟩
      rw [← Nat.prod_primeFactorsList hb, ← hu1.prod_eq, ← prod_replicate]
      exact hu2.prod_dvd_prod

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (H ⊓ K).relIndex ⊤ ≤ H.relIndex ⊤ * K.relIndex ⊤

Tactic:
relIndex_inf_le

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
X : Type u_3
inst✝¹ : MulAction G X
inst✝ : Finite (MulAction.orbitRel.Quotient G X)
hi : H.index ≠ 0
⊢ Finite (MulAction.orbitRel.Quotient (↥H) X)

Tactic:
have := fintypeOfIndexNeZero hi

Goal state after:
G : Type u_1
inst✝² : Group G
H : Subgroup G
X : Type u_3
inst✝¹ : MulAction G X
inst✝ : Finite (MulAction.orbitRel.Quotient G X)
hi : H.index ≠ 0
this : Fintype (G ⧸ H)
⊢ Finite (MulAction.orbitRel.Quotient (↥H) X)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ℤ
⊢ (↑a).cast = a % ↑n

Tactic:
by
  cases n
  · rw [Int.ofNat_zero, Int.emod_zero, Int.cast_id]; rfl
  · rw [← val_intCast, val]; rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x + 1 < 0
hn : 1 < n
⊢ if Even n then ∑ i ∈ range n, x ^ i < 0 else 1 < ∑ i ∈ range n, x ^ i

Tactic:
have hx0 : x < 0 := (le_add_of_nonneg_right zero_le_one).trans_lt hx

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x + 1 < 0
hn : 1 < n
hx0 : x < 0
⊢ if Even n then ∑ i ∈ range n, x ^ i < 0 else 1 < ∑ i ∈ range n, x ^ i
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ ↑(Nat.chineseRemainder h x.cast.1.val x.cast.2.val) ≡ x.val [MOD m * n]

Tactic:
← Nat.modEq_and_modEq_iff_modEq_mul h,

Goal state after:
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ ↑(Nat.chineseRemainder h x.cast.1.val x.cast.2.val) ≡ x.val [MOD m] ∧
    ↑(Nat.chineseRemainder h x.cast.1.val x.cast.2.val) ≡ x.val [MOD n]
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inr
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
⊢ b.digits n ++ b.digits m = b.digits (ofDigits b (b.digits n ++ b.digits m))

Tactic:
refine (digits_ofDigits b hb _ (fun l hl => ?_) (fun h_append => ?_)).symm

Goal state after:
case inr.refine_1
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
l : ℕ
hl : l ∈ b.digits n ++ b.digits m
⊢ l < b

case inr.refine_2
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
h_append : b.digits n ++ b.digits m ≠ []
⊢ (b.digits n ++ b.digits m).getLast h_append ≠ 0
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) + ∑ k ∈ Ico 1 tl.length, ofDigits p (List.drop k tl) +
        ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
← add_zero (∑ x ∈ Ico _ _, ofDigits p (tl.drop x)),

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) + 0) +
        ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case bit.false
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits
⊢ 0 < bit false n

Tactic:
simpa [Nat.bit, pos_iff_ne_zero]

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

Goal state before:
pp: n : ℕ
⊢ digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits

Tactic:
by
  induction n using Nat.binaryRecFromOne with
  | zero => simp
  | one => simp
  | bit b n h ih =>
    rw [bits_append_bit _ _ fun hn => absurd hn h]
    cases b
    · rw [digits_def' one_lt_two]
      · simpa [Nat.bit]
      · simpa [Nat.bit, pos_iff_ne_zero]
    · simpa [Nat.bit, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]

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

Goal state before:
pp: case ind.zero
b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
⊢ ((b + 2).digits n.succ).head?.getD 0 = n.succ / (b + 2) ^ 0 % (b + 2)

Tactic:
← default_eq_zero,

Goal state after:
case ind.zero
b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
⊢ ((b + 2).digits n.succ).head?.getD default = n.succ / (b + 2) ^ default % (b + 2)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: η : Type u_6
Gs : η → Type u_7
inst✝ : (i : η) → Monoid (Gs i)
x : (i : η) → Gs i
h : IsOfFinOrder x
⊢ ∀ (i : η), IsOfFinOrder (x i)

Tactic:
by
  obtain ⟨n, npos, hn⟩ := h.exists_pow_eq_one
  exact fun _ => isOfFinOrder_iff_pow_eq_one.mpr ⟨n, npos, (congr_fun hn.symm _).symm⟩

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a - b) = emultiplicity p b

Tactic:
rw [sub_eq_add_neg, emultiplicity_add_of_gt] <;> rw [emultiplicity_neg]

Goal state after:
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p b < emultiplicity p a
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l d : ℕ
w✝ : List ℕ
left✝ : w✝ ∈ fixedLengthDigits hb l
hL : d :: w✝ ∈ consFixedLengthDigits hb l d
⊢ (d :: w✝).head ⋯ = d

Tactic:
head_cons

Goal state after:
b : ℕ
hb : 1 < b
l d : ℕ
w✝ : List ℕ
left✝ : w✝ ∈ fixedLengthDigits hb l
hL : d :: w✝ ∈ consFixedLengthDigits hb l d
⊢ d = d
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case succ.inr
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
hn : n ≠ 0
⊢ (n * n ^ k).factorization = (k + 1) • n.factorization

Tactic:
factorization_mul hn (pow_ne_zero _ hn),

Goal state after:
case succ.inr
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
hn : n ≠ 0
⊢ n.factorization + (n ^ k).factorization = (k + 1) • n.factorization
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
refine ⟨factorization_eq_zero_of_remainder i, fun h => ?_⟩

Goal state after:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : (p * i + r).factorization p = 0
⊢ ¬p ∣ r
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ emultiplicity p (p ^ n) = ↑n

Tactic:
apply emultiplicity_eq_of_dvd_of_not_dvd
  · rfl
  · rw [pow_dvd_pow_iff h0 hu]
    apply Nat.not_succ_le_self

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

Goal state before:
pp: case inr
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ a.factorization ≤ (a * b).factorization

Tactic:
factorization_le_iff_dvd ha <| mul_ne_zero ha hb

Goal state after:
case inr
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ a ∣ a * b
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
a : G
ha : IsOfFinOrder a
⊢ (↑(powers a)).Finite

Tactic:
ha.powers_eq_image_range_orderOf

Goal state after:
G : Type u_1
inst✝ : Monoid G
a : G
ha : IsOfFinOrder a
⊢ (↑(Finset.image (fun x ↦ a ^ x) (Finset.range (orderOf a)))).Finite
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : d = 0
⊢ d ∣ n / p ^ n.factorization p

Tactic:
simp [hd0] at hpd

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

Goal state before:
pp: case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
⊢ (x + y) ^ p = x ^ p + y ^ p

Tactic:
let ⟨r, hr⟩ := h.exists_add_pow_prime_eq hprime
    simp [hr]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
hG : ∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a
⊢ IsMulTorsionFree G

Tactic:
refine ⟨fun n hn a b hab ↦ ?_⟩
    rw [← div_eq_one] at hab ⊢
    simp only [← div_pow, isOfFinOrder_iff_pow_eq_one] at hab hG
    exact of_not_not fun hab' ↦ hG hab' ⟨n, hn.bot_lt, hab⟩

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
a : G
x : k[G]
a✝ : G
⊢ (of' k G a * x /ᵒᶠ a).coeff a✝ = x.coeff a✝

Tactic:
simp only [of'_apply, coeff_divOf, coeff_single_mul_add, one_mul]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case inr
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ (single g 1 * (x /ᵒᶠ g)).coeff g' + (x %ᵒᶠ g).coeff g' = x.coeff g'

Tactic:
· rw [coeff_modOf_of_not_exists_add x _ _ h, coeff_single_mul_of_forall_add_ne, zero_add]
    simpa [eq_comm] using h

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
⊢ f = (⇑(expand R p))^[Nat.zero] f

Tactic:
Function.iterate_zero,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
⊢ f = id f
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
hpn : p ∣ n
⊢ f.coeff (n / p) = 0

Tactic:
coeff_eq_zero_of_natDegree_lt

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
hpn : p ∣ n
⊢ 0 = 0

case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
hpn : p ∣ n
⊢ f.natDegree < n / p
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
⊢ (expand R p) (contract p f) = f

Tactic:
by
  obtain _ | @⟨_, hprime, hchar⟩ := ‹ExpChar R p›
  · rw [expand_one, contract_one]
  · have := Fact.mk hchar; exact expand_contract p hf hprime.ne_zero

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hmo : q.Monic
a✝ : Nontrivial R
⊢ 0 + q * p = q * p

Tactic:
rw [zero_add]

Goal state after: