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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
x✝ : ℕ
hf : #f.support = x✝
⊢ motive f

Tactic:
induction hf : #f.support generalizing f with

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
⊢ (eval (Fin.cons y s)) f = Polynomial.eval y (Polynomial.map (eval s) ((finSuccEquiv R n) f))

Tactic:
by
  -- turn this into a def `Polynomial.mapAlgHom`
  let φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
    { Polynomial.mapRingHom (eval s) with
      commutes' := fun r => by
        convert! Polynomial.map_C (eval s)
        exact (eval_C _).symm }
  change
    aeval (Fin.cons y s : Fin (n + 1) → R) f =
      (Polynomial.aeval y).comp (φ.comp (finSuccEquiv R n).toAlgHom) f
  congr 2
  apply MvPolynomial.algHom_ext
  rw [Fin.forall_iff_succ]
  simp only [aeval_X, Fin.cons_zero, AlgHom.coe_comp, Polynomial.coe_aeval_eq_eval,
    AlgHom.coe_mk, Polynomial.coe_mapRingHom, AlgEquiv.coe_toAlgHom,
    comp_apply, finSuccEquiv_apply, eval₂Hom_X', Fin.cases_zero, Polynomial.map_X,
    Polynomial.eval_X, Fin.cons_succ, Fin.cases_succ, Polynomial.map_C, eval_X, Polynomial.eval_C,
    implies_true, and_self, φ]

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

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

Tactic:
exact hi

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

Goal state before:
pp: case pos
R : Type u
n : ℕ
inst✝ : Semiring R
p : MonicDegreeEq R n
i : ℕ
hi : n ≤ i
h✝ : i = n
⊢ (↑p).coeff i = 1

Tactic:
simp_all [p.2.1, p.2.2 _ (hi.lt_of_ne (.symm _))]

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

Goal state before:
pp: case neg
R : Type u
n : ℕ
inst✝ : Semiring R
p : MonicDegreeEq R n
i : ℕ
hi : n ≤ i
h✝ : ¬i = n
⊢ (↑p).coeff i = 0

Tactic:
simp_all [p.2.1, p.2.2 _ (hi.lt_of_ne (.symm _))]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ∃ j₀, j₀.castSucc = j
⊢ k i < Function.extend Fin.castSucc k (fun x ↦ f.natDegree) j

Tactic:
obtain ⟨j, rfl⟩ := hj
        rwa [Fin.strictMono_castSucc.injective.extend_apply, hk.lt_iff_lt,
          ← Fin.castSucc_lt_castSucc_iff]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
hp : (map f p).Monic
⊢ f p.leadingCoeff = f 1

Tactic:
rw [← leadingCoeff_map_of_injective hf, hp.leadingCoeff, f.map_one]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
n✝ : ℕ
⊢ ∑ i ∈ antidiagonal n✝, ↑h.unit⁻¹ * (p.coeff i.1 * q.coeff i.2) =
    ∑ x ∈ antidiagonal n✝, ↑h.unit⁻¹ * p.coeff x.1 * q.coeff x.2

Tactic:
refine sum_congr rfl fun x _ => ?_

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
n✝ : ℕ
x : ℕ × ℕ
x✝ : x ∈ antidiagonal n✝
⊢ ↑h.unit⁻¹ * (p.coeff x.1 * q.coeff x.2) = ↑h.unit⁻¹ * p.coeff x.1 * q.coeff x.2
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝ : Semiring R
p : ℕ
h✝ : CharP R p
h : ∀ (x : ℕ), ↑x = 0 ↔ p ∣ x
n : ℕ
⊢ ↑n = 0 ↔ p ∣ n

Tactic:
by rw [← map_natCast C, ← C_0, C_inj, h]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑n
this : p.natDegree + (n - p.natDegree) = n
⊢ ↑p.natDegree + ↑(n - p.natDegree) ≤ ↑n

Tactic:
rw [← Nat.cast_add, this]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
hr : Prime r
⊢ Prime (C r)

Tactic:
have := hr.1
    rw [← Ideal.span_singleton_prime] at hr ⊢
    · rw [← Set.image_singleton, ← Ideal.map_span]
      infer_instance
    · intro h; apply (this (C_eq_zero.mp h))
    · assumption

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

Goal state before:
pp: n a b c : ℤ
⊢ a + n * b ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

Tactic:
add_modulus_mul_modEq_iff

Goal state after:
n a b c : ℤ
⊢ a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c : ℤ
⊢ n * b + a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

Tactic:
by
  rw [add_comm, add_modulus_mul_modEq_iff]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℤ
⊢ ↑a = ↑b ↔ a ≡ b [ZMOD ↑p]

Tactic:
by
  rw [eq_comm, ← sub_eq_zero, ← Int.cast_sub, CharP.intCast_eq_zero_iff R p, Int.modEq_iff_dvd]

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

Goal state before:
pp: case inr
j : ℕ
left✝ : Prime j
a1 : 1 ≠ 1
hp : Prime (1 * j)
⊢ 1 * j = 1

Tactic:
· exact (a1 rfl).elim

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

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ Even p ↔ ¬3 ≤ p

Tactic:
hp.even_iff,

Goal state after:
p : ℕ
hp : Prime p
⊢ p = 2 ↔ ¬3 ≤ p
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ A ∙ (mk I) 1 = Submodule.map (Submodule.mkQ I) (span {1})

Tactic:
Ideal.span,

Goal state after:
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ A ∙ (mk I) 1 = Submodule.map (Submodule.mkQ I) (A ∙ 1)
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case mk.mk
A : Type u_3
inst✝³ : Ring A
R : Type u_5
inst✝² : CommRing R
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : Algebra R A
a₁✝ : R ⧸ comap (algebraMap R A) I
a : R
a₂✝ : R ⧸ comap (algebraMap R A) I
b : R
hab : (algebraMap R A) a - (algebraMap R A) b ∈ I
⊢ Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) a =
    Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) b

Tactic:
← map_sub

Goal state after:
case mk.mk
A : Type u_3
inst✝³ : Ring A
R : Type u_5
inst✝² : CommRing R
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : Algebra R A
a₁✝ : R ⧸ comap (algebraMap R A) I
a : R
a₂✝ : R ⧸ comap (algebraMap R A) I
b : R
hab : (algebraMap R A) (a - b) ∈ I
⊢ Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) a =
    Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) b
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case inl
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
⊢ IsPeriodicPt f (m - n) x

Tactic:
refine left_of_add ?_ hn
    rwa [tsub_add_cancel_of_le h]

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 : Set A
hcomm✝ : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : adjoin R s ≤ centralizer R ↑(centralizer R s)
x✝¹ x✝ : A
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : x✝¹ ∈ ↑(centralizer R ↑(centralizer R s))
h₂ : x✝ ∈ ↑(centralizer R ↑(centralizer R s))
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
coe_centralizer_centralizer

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 : Set A
hcomm✝ : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : adjoin R s ≤ centralizer R ↑(centralizer R s)
x✝¹ x✝ : A
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : x✝¹ ∈ (s ∪ star s).centralizer.centralizer
h₂ : x✝ ∈ (s ∪ star s).centralizer.centralizer
⊢ x✝¹ * x✝ = x✝ * x✝¹
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ ∀ (c : ℕ), minimalPeriod (Prod.map f g) x ∣ c ↔ (minimalPeriod f x.1).lcm (minimalPeriod g x.2) ∣ c

Tactic:
simp [← isPeriodicPt_iff_minimalPeriod_dvd, Nat.lcm_dvd_iff]

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
⊢ minimalPeriod (Pi.map f) x = sInf {n | n > 0 ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}

Tactic:
conv_lhs => simp [minimalPeriod_eq_sInf_n_pos_IsPeriodicPt]

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
⊢ sInf {n | 0 < n ∧ ∀ (i : ι), IsPeriodicPt (f i) n (x i)} = sInf {n | n > 0 ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ g ∈ stabilizer G s

Tactic:
mem_stabilizer_iff

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ g • s = s
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case inl
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
H : Subgroup G
inst✝ : Finite (G ⧸ H)
he : IsEmpty X
⊢ Finite (orbitRel.Quotient (↥H) X)

pp: case inr
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
H : Subgroup G
inst✝ : Finite (G ⧸ H)
b : X
⊢ Finite (orbitRel.Quotient (↥H) X)

Tactic:
· exact Quotient.finite _

Goal state after:
case inr
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
H : Subgroup G
inst✝ : Finite (G ⧸ H)
b : X
⊢ Finite (orbitRel.Quotient (↥H) X)
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 (ConjAct G) / Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct G) g, Nat.mul_div_cancel]

Goal state after:
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 ↑(MulAction.orbit (ConjAct G) g)

case H
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)
⊢ 0 < Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList

Tactic:
rw [mem_primeFactorsList (mul_ne_zero ha hb), mem_primeFactorsList ha, mem_primeFactorsList hb,
    ← and_or_left]
  simpa only [and_congr_right_iff] using Prime.dvd_mul

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (J ⊓ L).relIndex (K ⊓ L) ≠ 0

Tactic:
rw [← range_subtype L, inf_comm, ← map_comap_eq, inf_comm, ← map_comap_eq, ← relIndex_comap,
    comap_map_eq_self_of_injective (subtype_injective L)]

Goal state after:
G : Type u_1
inst✝ : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (comap L.subtype J).relIndex (comap L.subtype K) ≠ 0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.relIndex K ∣ 2 ↔ ∃ a ∈ K, ∀ b ∈ K, a * b ∈ H ∨ b ∈ H

Tactic:
by
  simp [Subgroup.relIndex, Subgroup.index_dvd_two_iff', mem_subgroupOf]

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

Goal state before:
pp: n : ℕ
⊢ val 2 = 2 % n

Tactic:
by
  rw [← Nat.cast_two, val_natCast]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
n : ℕ
hmn✝ : 2 ≤ n
ihn : 0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1
⊢ -x * ∑ i ∈ range n, x ^ i < 1 ∧ x * ∑ i ∈ range n, x ^ i < 0

Tactic:
exact
    ⟨mul_lt_one_of_nonneg_of_lt_one_left (neg_nonneg.2 hx.le) (neg_lt_iff_pos_add'.2 hx') ihn.2.le,
      mul_neg_of_neg_of_pos hx ihn.1⟩

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

Goal state before:

Tactic:
a * a⁻¹ = a * a⁻¹ + n.succ * Nat.gcdB (val a) n.succ := by
        rw [natCast_self, zero_mul, add_zero]
      _ = ↑(↑a.val * Nat.gcdA (val a) n.succ + n.succ * Nat.gcdB (val a) n.succ) := by
        push_cast
        rw [natCast_zmod_val]
        rfl
      _ = Nat.gcd a.val n.succ := by rw [← Nat.gcd_eq_gcd_ab a.val n.succ]; rfl

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

Goal state before:
pp: n : ℤ
⊢ ↑n = 1 ↔ Odd n

Tactic:
by
  rw [← Int.cast_one, ZMod.intCast_eq_intCast_iff, Int.odd_iff, Int.ModEq]
  simp

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

Goal state before:
pp: n : ℕ
u : (ZMod n)ˣ
⊢ (↑u)⁻¹ = ↑u⁻¹

Tactic:
have := congr_arg ((↑) : ℕ → ZMod n) (val_coe_unit_coprime u)
  rw [← mul_inv_eq_gcd, Nat.cast_one] at this
  exact (Units.inv_eq_of_mul_eq_one_right this).symm

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

Goal state before:
pp: case cons
b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ tl.length * ofDigits b l2
⊢ ofDigits b (hd :: tl ++ l2) = ofDigits b (hd :: tl) + b ^ (hd :: tl).length * ofDigits b l2

Tactic:
rw [ofDigits, List.cons_append, ofDigits, IH, List.length_cons, pow_succ']
    ring

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

Goal state before:
pp: case succ.succ.ind.zero
b : ℕ
h : ∀ m < 0, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits 0) = 0

Tactic:
rw [digits_zero]

Goal state after:
case succ.succ.ind.zero
b : ℕ
h : ∀ m < 0, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) [] = 0
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ}, L.length = L2.length → (∀ l ∈ L, l < b) → (∀ l ∈ L2, l < b) → ofDigits b L = ofDigits b L2 → L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
w2 : ∀ l_1 ∈ d :: l, l_1 < b
h : D + b * ofDigits b L = d + b * ofDigits b l
len : L.length = l.length
eqd : D = d
⊢ D :: L = d :: l

Tactic:
simp only [eqd, add_right_inj, mul_left_cancel_iff_of_pos (zero_lt_of_lt hb)] at h

Goal state after:
case cons
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ}, L.length = L2.length → (∀ l ∈ L, l < b) → (∀ l ∈ L2, l < b) → ofDigits b L = ofDigits b L2 → L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
w2 : ∀ l_1 ∈ d :: l, l_1 < b
len : L.length = l.length
eqd : D = d
h : ofDigits b L = ofDigits b l
⊢ D :: L = d :: l
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case succ.succ
m : ℕ
hm : m ≠ 0
b : ℕ
⊢ ((b + 1 + 1).digits m).getLast ⋯ ≠ 0

Tactic:
revert hm

Goal state after:
case succ.succ
m b : ℕ
⊢ ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
Module: Mathlib.Data.Nat.Digits.Lemmas

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

pp: 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

Tactic:
· rcases (List.mem_append.mp hl) with (h | h) <;> exact digits_lt_base hb h

Goal state after:
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.Defs

Goal state before:
pp: case ind.zero
b d : ℕ
IH : ∀ m < 0, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ []
⊢ d < b + 2

Tactic:
cases hd

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

Goal state before:
pp: case ind.succ
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))
⊢ d < b + 2

Tactic:
cases hd

Goal state after:
case ind.succ.head
b n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
⊢ (n + 1) % (b + 2) < b + 2

case ind.succ.tail
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
a✝ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ d < b + 2
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)

Goal state after:
p i n : ℕ
h : 2 ≤ p
⊢ n = ofDigits p (p.digits n)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case neg
α : Type u_1
inst✝ : Monoid α
a b : α
hf : ¬FiniteMultiplicity a b
⊢ ↑(multiplicity a b) ≤ emultiplicity a b

Tactic:
simp [hf, emultiplicity_eq_top.2]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
⊢ emultiplicity a b ≤ emultiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

Tactic:
classical
  constructor
  · exact fun h n hab ↦ pow_dvd_of_le_emultiplicity (le_trans (le_emultiplicity_of_pow_dvd hab) h)
  · intro h
    unfold emultiplicity
    -- aesop? says
    split
    next h_1 =>
      obtain ⟨w, h_1⟩ := h_1
      split
      next h_2 =>
        simp_all only [cast_le, le_find_iff, lt_find_iff, Decidable.not_not, le_refl,
          not_true_eq_false, not_false_eq_true, implies_true]
      next h_2 => simp_all only [not_exists, Decidable.not_not, le_top]
    next h_1 =>
      simp_all only [not_exists, Decidable.not_not, not_true_eq_false, top_le_iff,
        dite_eq_right_iff, ENat.natCast_ne_top, imp_false, not_false_eq_true, implies_true]

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ Finset (List ℕ)

Tactic:
have : Fintype {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} :=
    Fintype.ofInjective (Set.MapsTo.restrict _ _ _ (mapsTo_ofDigits hb l))
      <| (Set.MapsTo.restrict_inj (mapsTo_ofDigits hb l)).mpr <| injOn_ofDigits hb l

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
this : Fintype ↑{L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ Finset (List ℕ)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : 1 = a * v
⊢ False

Tactic:
have : IsUnit a := .of_mul_eq_one v hv.symm
      simpa [this] using ha.not_isUnit

Goal state after:
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 • (b * (b - 1) / 2) + (Finset.range b).card • ∑ x ∈ fixedLengthDigits hb l, x.sum =
    (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
hr,

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 • (l * b ^ (l - 1) * b.choose 2) =
    (l + 1) * b ^ (l + 1 - 1) * b.choose 2
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : ¬FiniteMultiplicity p (a * b)
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b

Tactic:
rw [emultiplicity_eq_top.mpr hfin, eq_comm, ENat.add_eq_top, emultiplicity_eq_top,
      emultiplicity_eq_top]
    simpa only [FiniteMultiplicity.mul_iff hp, not_and_or] using hfin

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ orderOf (-1) = 2

Tactic:
apply orderOf_eq_prime

Goal state after:
case neg.hg
R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ (-1) ^ 2 = 1

case hg1
R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ -1 ≠ 1
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
hm : emultiplicity p (p * n)! ≠ ⊤
⊢ emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1

Tactic:
revert hm

Goal state after:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ emultiplicity p (p * n)! ≠ ⊤ → emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1
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

Goal state after:
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
r : R
hr : (x + y) ^ p = x ^ p + y ^ p + ↑p * x * y * r
⊢ (x + y) ^ p = x ^ p + y ^ p
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
⊢ e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
apply dvd_prod_pow_of_factorization_le he_pos

Goal state after:
case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
⊢ e.factorization ≤ a.factorization ⊓ b.factorization
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
n : ℤ
⊢ x ^ n = 1 ↔ n ≡ 0 [ZMOD ↑(orderOf x)]

Tactic:
rw [Int.modEq_zero_iff_dvd, orderOf_dvd_iff_zpow_eq_one]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p n : ℕ
inst✝ : ExpChar R p
x✝ : R
⊢ (iterateFrobenius R p n) x✝ = (frobenius R p ^ n) x✝

Tactic:
simp [iterateFrobenius_def, iterate_frobenius]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
hS : S.Nonempty
⊢ 1 ∈ S ^ card G

Tactic:
obtain ⟨a, ha⟩ := hS
    rw [← pow_card_eq_one]
    exact Set.pow_mem_pow ha

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

Goal state before:
pp: case h
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
⊢ a = c ^ n

Tactic:
apply eq_of_factorization_eq ha0 (by simp [c, factors])

Goal state after:
case h
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := ⋯
c : ℕ := ⋯
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
⊢ ∀ (p : ℕ), a.factorization p = (c ^ n).factorization p